Theorem bitr3id 194

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

Hypotheses

Ref	Expression
bitr3id.1	|- ( ps <-> ph )
bitr3id.2	|- ( ch -> ( ps <-> th ) )

Assertion

Ref	Expression
bitr3id	|- ( ch -> ( ph <-> th ) )

Proof of Theorem bitr3id

Step	Hyp	Ref	Expression
1		bitr3id.1	. . 3 |- ( ps <-> ph )
2	1	bicomi 132	. 2 |- ( ph <-> ps )
3		bitr3id.2	. 2 |- ( ch -> ( ps <-> th ) )
4	2, 3	bitrid 192	1 |- ( ch -> ( ph <-> th ) )

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  900  19.16  1566  19.19  1677  cbvab  2313  necon1bbiidc  2421  rspc2gv  2872  elabgt  2897  sbceq1a  2991  sbcralt  3058  sbcrext  3059  sbccsbg  3105  sbccsb2g  3106  iunpw  4505  tfis  4607  xp11m  5092  ressn  5194  fnssresb  5354  fun11iun  5508  funimass4  5594  dffo4  5692  f1ompt  5695  fliftf  5828  resoprab2  6001  ralrnmpo  6019  rexrnmpo  6020  1stconst  6254  2ndconst  6255  dfsmo2  6320  smoiso  6335  brecop  6659  ixpsnf1o  6770  ac6sfi  6934  ismkvnex  7193  nninfwlporlemd  7210  prarloclemn  7538  axcaucvglemres  7938  reapti  8577  indstr  9635  iccneg  10031  sqap0  10633  sqrt00  11096  minclpr  11292  fprodseq  11638  absefib  11825  efieq1re  11826  prmind2  12169  gsumval2  12890  eqgval  13195  sincosq3sgn  14785  sincosq4sgn  14786  lgsdinn0  14986  pw1nct  15290  iswomninnlem  15336