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 ⊢ (𝜒 → (𝜑 ↔ 𝜃))

Syntax hints:   → wi 4   ↔ wb 105

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  3bitr3g  222  imbibi  252  ianordc  906  19.16  1603  19.19  1713  cbvab  2354  necon1bbiidc  2462  rspc2gv  2921  elabgt  2946  sbceq1a  3040  sbcralt  3107  sbcrext  3108  sbccsbg  3155  sbccsb2g  3156  iunpw  4579  tfis  4683  reldmm  4952  xp11m  5177  ressn  5279  fnssresb  5446  fun11iun  5607  funimass4  5699  dffo4  5798  f1ompt  5801  fliftf  5945  resoprab2  6123  ralrnmpo  6141  rexrnmpo  6142  1stconst  6391  2ndconst  6392  dfsmo2  6458  smoiso  6473  brecop  6799  ixpsnf1o  6910  ac6sfi  7092  ismkvnex  7359  nninfwlporlemd  7376  prarloclemn  7724  axcaucvglemres  8124  reapti  8764  indstr  9832  iccneg  10229  sqap0  10874  wrdmap  11154  wrdind  11312  sqrt00  11623  minclpr  11820  fprodseq  12167  absefib  12355  efieq1re  12356  prmind2  12715  gsumval2  13503  eqgval  13833  isnzr2  14222  sincosq3sgn  15581  sincosq4sgn  15582  fsumdvdsmul  15744  lgsdinn0  15806  pw1nct  16664  iswomninnlem  16721