Theorem bitr3d 408

Description: Deduction form of bitr3 153.

Hypotheses

Ref	Expression
bitr3d.1	⊢ (φ → (ψ ↔ χ))
bitr3d.2	⊢ (φ → (ψ ↔ θ))

Assertion

Ref	Expression
bitr3d	⊢ (φ → (χ ↔ θ))

Proof of Theorem bitr3d

Step	Hyp	Ref	Expression
1		bitr3d.1	. . 3 ⊢ (φ → (ψ ↔ χ))
2	1	bicomd 399	. 2 ⊢ (φ → (χ ↔ ψ))
3		bitr3d.2	. 2 ⊢ (φ → (ψ ↔ θ))
4	2, 3	bitrd 406	1 ⊢ (φ → (χ ↔ θ))

Syntax hints:   → wi 2   ↔ wb 127

This theorem is referenced by:  3bitr3d 423  sbequ12a 867  sbco2 913  sbco3 915  sbcom 916  sbcom2 992  sbal1 996  sbal 997  elabf 1414  sbc5g 1450  sbc6g 1451  sbcel1 1466  sbcel2 1467  sbcgf 1469  copsex2g 1903  iununi 2037  opabsb 2114  opelopabg 2115  ordtri2 2233  onmindif 2312  onmindif2 2313  dfom2 2374  fcnvres 2768  isocnv 2934  isoini 2938  oa00 3161  mapxpen 3390  omsucdom 3418  isfinite2 3437  unfilem1 3438  rankr1a 3521  r1val2 3522  bnd2 3549  fodomb 3615  domtri 3644  iscard 3659  suplem2pr 3956  addcan2t 4123  ltsub13t 4360  ltmuldiv2t 4407  lt2sq 4414  nn1suc 4435  nnsub 4450  elnn0nn 4593  elnnnn0 4594  uzind 4603  zbtwnre 4619  om2uzlt 4654  sqrsq 4764  znnen 4930  hi2eqt 5059  ch0psst 5370  pjelt 5668  jp 5703  chcv2t 5752  cvp 5764  atnem0 5766

This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-3 5  ax-mp 6

This theorem depends on definitions:  df-bi 128  df-an 198

metamath.org