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  1706  eueq3dc  2886  sbcel12g  3046  sbceqg  3047  sbcnel12g  3048  reldisj  3445  r19.3rm  3482  eldifpr  3587  eldiftp  3605  rabxp  4620  elrng  4774  iss  4909  eliniseg  4953  fcnvres  5350  dffv3g  5461  funimass4  5516  fndmdif  5569  fneqeql  5572  funimass3  5580  elrnrexdmb  5604  dff4im  5610  fconst4m  5684  elunirn  5711  riota1  5792  riota2df  5794  f1ocnvfv3  5807  eqfnov  5921  caoftrn  6051  mpoxopovel  6182  rntpos  6198  ordgt0ge1  6376  iinerm  6545  erinxp  6547  qliftfun  6555  mapdm0  6601  elfi2  6909  fifo  6917  inl11  6999  ctssdccl  7045  isomnimap  7063  ismkvmap  7080  iswomnimap  7092  omniwomnimkv  7093  pr2nelem  7109  indpi  7245  genpdflem  7410  genpdisj  7426  genpassl  7427  genpassu  7428  ltnqpri  7497  ltpopr  7498  ltexprlemm  7503  ltexprlemdisj  7509  ltexprlemloc  7510  ltrennb  7757  letri3  7941  letr  7943  ltneg  8320  leneg  8323  reapltxor  8447  apsym  8464  suprnubex  8807  suprleubex  8808  elnnnn0  9116  zrevaddcl  9200  znnsub  9201  znn0sub  9215  prime  9246  eluz2  9428  eluz2b1  9494  nn01to3  9508  qrevaddcl  9535  xrletri3  9691  xrletr  9694  iccid  9811  elicopnf  9855  fzsplit2  9934  fzsn  9950  fzpr  9961  uzsplit  9976  fvinim0ffz  10122  lt2sqi  10488  le2sqi  10489  abs00ap  10944  iooinsup  11156  mertenslem2  11415  fprod2dlemstep  11501  gcddiv  11883  algcvgblem  11906  isprm3  11975  phisum  12092  eltg2b  12414  discld  12496  opnssneib  12516  restbasg  12528  ssidcn  12570  cnptoprest2  12600  lmss  12606  txrest  12636  txlm  12639  imasnopn  12659  bldisj  12761  xmeter  12796  bl2ioo  12902  limcdifap  12991  bj-sseq  13325  nnti  13526  pw1nct  13535