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  1364  3biant1d  1367  equsalh  1750  eueq3dc  2951  sbcel12g  3112  sbceqg  3113  sbcnel12g  3114  reldisj  3516  r19.3rm  3553  eldifpr  3665  eldiftp  3684  rabxp  4720  elrng  4877  iss  5014  eliniseg  5061  fcnvres  5471  dffv3g  5585  funimass4  5642  fndmdif  5698  fneqeql  5701  funimass3  5709  elrnrexdmb  5733  dff4im  5739  fconst4m  5817  elunirn  5848  riota1  5931  riota2df  5933  f1ocnvfv3  5946  eqfnov  6065  caoftrn  6204  mpoxopovel  6340  rntpos  6356  ordgt0ge1  6534  iinerm  6707  erinxp  6709  qliftfun  6717  mapdm0  6763  elfi2  7089  fifo  7097  inl11  7182  ctssdccl  7228  isomnimap  7254  ismkvmap  7271  iswomnimap  7283  omniwomnimkv  7284  pr2nelem  7314  indpi  7475  genpdflem  7640  genpdisj  7656  genpassl  7657  genpassu  7658  ltnqpri  7727  ltpopr  7728  ltexprlemm  7733  ltexprlemdisj  7739  ltexprlemloc  7740  ltrennb  7987  letri3  8173  letr  8175  ltneg  8555  leneg  8558  reapltxor  8682  apsym  8699  suprnubex  9046  suprleubex  9047  elnnnn0  9358  zrevaddcl  9443  znnsub  9444  znn0sub  9458  prime  9492  eluz2  9674  eluz2b1  9742  nn01to3  9758  qrevaddcl  9785  xrletri3  9946  xrletr  9950  iccid  10067  elicopnf  10111  fzsplit2  10192  fzsn  10208  fzpr  10219  uzsplit  10234  fvinim0ffz  10392  lt2sqi  10794  le2sqi  10795  ccatlcan  11194  ccatrcan  11195  abs00ap  11448  iooinsup  11663  mertenslem2  11922  fprod2dlemstep  12008  gcddiv  12415  algcvgblem  12446  isprm3  12515  dvdsfi  12636  imasmnd2  13359  imasgrp2  13521  issubg  13584  resgrpisgrp  13606  eqgval  13634  imasrng  13793  ring1  13896  imasring  13901  crngunit  13948  lssle0  14209  lssats2  14251  zndvds  14486  znleval  14490  znleval2  14491  eltg2b  14601  discld  14683  opnssneib  14703  restbasg  14715  ssidcn  14757  cnptoprest2  14787  lmss  14793  txrest  14823  txlm  14826  imasnopn  14846  bldisj  14948  xmeter  14983  bl2ioo  15097  limcdifap  15209  bj-sseq  15867  nnti  16068  2omap  16071  pw1nct  16081