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  2978  sbcel12g  3140  sbceqg  3141  sbcnel12g  3142  reldisj  3544  r19.3rm  3581  eldifpr  3694  eldiftp  3713  rabxp  4761  elrng  4919  iss  5057  eliniseg  5104  fcnvres  5517  dffv3g  5631  funimass4  5692  fndmdif  5748  fneqeql  5751  funimass3  5759  elrnrexdmb  5783  dff4im  5789  fconst4m  5869  elunirn  5902  riota1  5986  riota2df  5988  f1ocnvfv3  6002  eqfnov  6123  caoftrn  6263  mpoxopovel  6402  rntpos  6418  ordgt0ge1  6598  iinerm  6771  erinxp  6773  qliftfun  6781  mapdm0  6827  elfi2  7162  fifo  7170  inl11  7255  ctssdccl  7301  isomnimap  7327  ismkvmap  7344  iswomnimap  7356  omniwomnimkv  7357  pr2nelem  7387  indpi  7552  genpdflem  7717  genpdisj  7733  genpassl  7734  genpassu  7735  ltnqpri  7804  ltpopr  7805  ltexprlemm  7810  ltexprlemdisj  7816  ltexprlemloc  7817  ltrennb  8064  letri3  8250  letr  8252  ltneg  8632  leneg  8635  reapltxor  8759  apsym  8776  suprnubex  9123  suprleubex  9124  elnnnn0  9435  zrevaddcl  9520  znnsub  9521  znn0sub  9535  prime  9569  eluz2  9751  eluz2b1  9825  nn01to3  9841  qrevaddcl  9868  xrletri3  10029  xrletr  10033  iccid  10150  elicopnf  10194  fzsplit2  10275  fzsn  10291  fzpr  10302  uzsplit  10317  fvinim0ffz  10477  lt2sqi  10879  le2sqi  10880  ccatlcan  11289  ccatrcan  11290  abs00ap  11613  iooinsup  11828  mertenslem2  12087  fprod2dlemstep  12173  gcddiv  12580  algcvgblem  12611  isprm3  12680  dvdsfi  12801  imasmnd2  13525  imasgrp2  13687  issubg  13750  resgrpisgrp  13772  eqgval  13800  imasrng  13959  ring1  14062  imasring  14067  crngunit  14115  lssle0  14376  lssats2  14418  zndvds  14653  znleval  14657  znleval2  14658  eltg2b  14768  discld  14850  opnssneib  14870  restbasg  14882  ssidcn  14924  cnptoprest2  14954  lmss  14960  txrest  14990  txlm  14993  imasnopn  15013  bldisj  15115  xmeter  15150  bl2ioo  15264  limcdifap  15376  bj-sseq  16324  nnti  16527  2omap  16530  pw1nct  16540