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  8907  indstr  9993  iccneg  10391  sqap0  11043  wrdmap  11336  wrdind  11494  sqrt00  11806  minclpr  12003  fprodseq  12350  absefib  12538  efieq1re  12539  prmind2  12898  ballotfilemsima  13259  gzsumval2  13714  eqgval  14026  isnzr2  14491  sincosq3sgn  15930  sincosq4sgn  15931  fsumdvdsmul  16109  lgsdinn0  16171  pw1nct  17037  iswomninnlem  17103