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  907  19.16  1604  19.19  1714  cbvab  2360  necon1bbiidc  2475  rspc2gv  2936  elabgt  2961  sbceq1a  3055  sbcralt  3122  sbcrext  3123  sbccsbg  3170  sbccsb2g  3171  iunpw  4606  tfis  4710  reldmm  4980  xp11m  5206  ressn  5308  fnssresb  5475  fun11iun  5640  funimass4  5732  dffo4  5830  f1ompt  5833  dfimafnf  5928  fliftf  5978  resoprab2  6158  ralrnmpo  6176  rexrnmpo  6177  1stconst  6430  2ndconst  6431  dfsmo2  6531  smoiso  6546  brecop  6872  ixpsnf1o  6984  ac6sfi  7168  ismkvnex  7459  nninfwlporlemd  7476  prarloclemn  7830  axcaucvglemres  8230  reapti  8870  indstr  9943  iccneg  10341  sqap0  10992  wrdmap  11281  wrdind  11439  sqrt00  11750  minclpr  11947  fprodseq  12294  absefib  12482  efieq1re  12483  prmind2  12842  ballotfilemsima  13203  gsumval2  13694  eqgval  14024  isnzr2  14414  sincosq3sgn  15805  sincosq4sgn  15806  fsumdvdsmul  15971  lgsdinn0  16033  pw1nct  16889  iswomninnlem  16946