Theorem bitr4di 198

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

Hypotheses

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

Assertion

Ref	Expression
bitr4di	|- ( ph -> ( ps <-> th ) )

Proof of Theorem bitr4di

Step	Hyp	Ref	Expression
1		bitr4di.1	. 2 |- ( ph -> ( ps <-> ch ) )
2		bitr4di.2	. . 3 |- ( th <-> ch )
3	2	bicomi 132	. 2 |- ( ch <-> th )
4	1, 3	bitrdi 196	1 |- ( ph -> ( ps <-> 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:  3bitr4g  223  bibi2i  227  3bior1fd  1386  3biant1d  1389  equsalh  1772  eueq3dc  2977  sbcel12g  3139  sbceqg  3140  sbcnel12g  3141  reldisj  3543  r19.3rm  3580  eldifpr  3693  eldiftp  3712  rabxp  4756  elrng  4913  iss  5051  eliniseg  5098  fcnvres  5511  dffv3g  5625  funimass4  5686  fndmdif  5742  fneqeql  5745  funimass3  5753  elrnrexdmb  5777  dff4im  5783  fconst4m  5863  elunirn  5896  riota1  5980  riota2df  5982  f1ocnvfv3  5996  eqfnov  6117  caoftrn  6257  mpoxopovel  6393  rntpos  6409  ordgt0ge1  6589  iinerm  6762  erinxp  6764  qliftfun  6772  mapdm0  6818  elfi2  7150  fifo  7158  inl11  7243  ctssdccl  7289  isomnimap  7315  ismkvmap  7332  iswomnimap  7344  omniwomnimkv  7345  pr2nelem  7375  indpi  7540  genpdflem  7705  genpdisj  7721  genpassl  7722  genpassu  7723  ltnqpri  7792  ltpopr  7793  ltexprlemm  7798  ltexprlemdisj  7804  ltexprlemloc  7805  ltrennb  8052  letri3  8238  letr  8240  ltneg  8620  leneg  8623  reapltxor  8747  apsym  8764  suprnubex  9111  suprleubex  9112  elnnnn0  9423  zrevaddcl  9508  znnsub  9509  znn0sub  9523  prime  9557  eluz2  9739  eluz2b1  9808  nn01to3  9824  qrevaddcl  9851  xrletri3  10012  xrletr  10016  iccid  10133  elicopnf  10177  fzsplit2  10258  fzsn  10274  fzpr  10285  uzsplit  10300  fvinim0ffz  10459  lt2sqi  10861  le2sqi  10862  ccatlcan  11265  ccatrcan  11266  abs00ap  11588  iooinsup  11803  mertenslem2  12062  fprod2dlemstep  12148  gcddiv  12555  algcvgblem  12586  isprm3  12655  dvdsfi  12776  imasmnd2  13500  imasgrp2  13662  issubg  13725  resgrpisgrp  13747  eqgval  13775  imasrng  13934  ring1  14037  imasring  14042  crngunit  14090  lssle0  14351  lssats2  14393  zndvds  14628  znleval  14632  znleval2  14633  eltg2b  14743  discld  14825  opnssneib  14845  restbasg  14857  ssidcn  14899  cnptoprest2  14929  lmss  14935  txrest  14965  txlm  14968  imasnopn  14988  bldisj  15090  xmeter  15125  bl2ioo  15239  limcdifap  15351  bj-sseq  16211  nnti  16415  2omap  16418  pw1nct  16428