Theorem bitr4di 197

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 131	. 2 |- ( ch <-> th )
4	1, 3	bitrdi 195	1 |- ( ph -> ( ps <-> th ) )

Syntax hints:   -> wi 4   <-> wb 104

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  3bitr4g  222  bibi2i  226  equsalh  1719  eueq3dc  2904  sbcel12g  3064  sbceqg  3065  sbcnel12g  3066  reldisj  3466  r19.3rm  3503  eldifpr  3610  eldiftp  3629  rabxp  4648  elrng  4802  iss  4937  eliniseg  4981  fcnvres  5381  dffv3g  5492  funimass4  5547  fndmdif  5601  fneqeql  5604  funimass3  5612  elrnrexdmb  5636  dff4im  5642  fconst4m  5716  elunirn  5745  riota1  5827  riota2df  5829  f1ocnvfv3  5842  eqfnov  5959  caoftrn  6086  mpoxopovel  6220  rntpos  6236  ordgt0ge1  6414  iinerm  6585  erinxp  6587  qliftfun  6595  mapdm0  6641  elfi2  6949  fifo  6957  inl11  7042  ctssdccl  7088  isomnimap  7113  ismkvmap  7130  iswomnimap  7142  omniwomnimkv  7143  pr2nelem  7168  indpi  7304  genpdflem  7469  genpdisj  7485  genpassl  7486  genpassu  7487  ltnqpri  7556  ltpopr  7557  ltexprlemm  7562  ltexprlemdisj  7568  ltexprlemloc  7569  ltrennb  7816  letri3  8000  letr  8002  ltneg  8381  leneg  8384  reapltxor  8508  apsym  8525  suprnubex  8869  suprleubex  8870  elnnnn0  9178  zrevaddcl  9262  znnsub  9263  znn0sub  9277  prime  9311  eluz2  9493  eluz2b1  9560  nn01to3  9576  qrevaddcl  9603  xrletri3  9761  xrletr  9765  iccid  9882  elicopnf  9926  fzsplit2  10006  fzsn  10022  fzpr  10033  uzsplit  10048  fvinim0ffz  10197  lt2sqi  10563  le2sqi  10564  abs00ap  11026  iooinsup  11240  mertenslem2  11499  fprod2dlemstep  11585  gcddiv  11974  algcvgblem  12003  isprm3  12072  phisum  12194  eltg2b  12848  discld  12930  opnssneib  12950  restbasg  12962  ssidcn  13004  cnptoprest2  13034  lmss  13040  txrest  13070  txlm  13073  imasnopn  13093  bldisj  13195  xmeter  13230  bl2ioo  13336  limcdifap  13425  bj-sseq  13827  nnti  14027  pw1nct  14036