Theorem bitr3id 194

Description: A syllogism inference from two biconditionals. (Contributed by NM, 5-Aug-1993.)

Hypotheses

Ref	Expression
bitr3id.1	⊢ (𝜓 ↔ 𝜑)
bitr3id.2	⊢ (𝜒 → (𝜓 ↔ 𝜃))

Assertion

Ref	Expression
bitr3id	⊢ (𝜒 → (𝜑 ↔ 𝜃))

Proof of Theorem bitr3id

Step	Hyp	Ref	Expression
1		bitr3id.1	. . 3 ⊢ (𝜓 ↔ 𝜑)
2	1	bicomi 132	. 2 ⊢ (𝜑 ↔ 𝜓)
3		bitr3id.2	. 2 ⊢ (𝜒 → (𝜓 ↔ 𝜃))
4	2, 3	bitrid 192	1 ⊢ (𝜒 → (𝜑 ↔ 𝜃))

This proof depends on syntax axioms:   → wi 4   ↔ wb 105

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117

This theorem is used by:  3bitr3g  222  imbibi  252  ianordc  911  19.16  1608  19.19  1718  cbvab  2364  necon1bbiidc  2481  rspc2gv  2942  elabgt  2967  sbceq1a  3061  sbcralt  3128  sbcrext  3129  sbccsbg  3176  sbccsb2g  3177  iunpw  4626  tfis  4730  reldmm  5000  xp11m  5226  ressn  5328  fnssresb  5495  fun11iun  5660  funimass4  5753  dffo4  5856  f1ompt  5859  dfimafnf  5955  fliftf  6005  resoprab2  6185  ralrnmpo  6203  rexrnmpo  6204  1stconst  6457  2ndconst  6458  dfsmo2  6558  smoiso  6573  brecop  6899  ixpsnf1o  7018  ac6sfi  7202  ismkvnex  7495  nninfwlporlemd  7512  prarloclemn  7866  axcaucvglemres  8266  reapti  8908  indstr  9995  iccneg  10393  sqap0  11045  wrdmap  11338  wrdind  11496  sqrt00  11808  minclpr  12005  fprodseq  12352  absefib  12540  efieq1re  12541  prmind2  12900  ballotfilemsima  13261  gzsumval2  13716  eqgval  14028  isnzr2  14493  sincosq3sgn  15932  sincosq4sgn  15933  fsumdvdsmul  16111  lgsdinn0  16179  pw1nct  17045  iswomninnlem  17111