Theorem 3bitr4d 220

Description: Deduction from transitivity of biconditional. Useful for converting conditional definitions in a formula. (Contributed by NM, 18-Oct-1995.)

Hypotheses

Ref	Expression
3bitr4d.1	|- ( ph -> ( ps <-> ch ) )
3bitr4d.2	|- ( ph -> ( th <-> ps ) )
3bitr4d.3	|- ( ph -> ( ta <-> ch ) )

Assertion

Ref	Expression
3bitr4d	|- ( ph -> ( th <-> ta ) )

Proof of Theorem 3bitr4d

Step	Hyp	Ref	Expression
1		3bitr4d.2	. 2 |- ( ph -> ( th <-> ps ) )
2		3bitr4d.1	. . 3 |- ( ph -> ( ps <-> ch ) )
3		3bitr4d.3	. . 3 |- ( ph -> ( ta <-> ch ) )
4	2, 3	bitr4d 191	. 2 |- ( ph -> ( ps <-> ta ) )
5	1, 4	bitrd 188	1 |- ( ph -> ( th <-> ta ) )

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:  dfbi3dc  1417  xordidc  1419  19.32dc  1702  r19.32vdc  2655  opbrop  4754  fvopab3g  5652  respreima  5708  fmptco  5746  cocan1  5856  cocan2  5857  brtposg  6340  nnmword  6604  swoer  6648  erth  6666  brecop  6712  ecopovsymg  6721  xpdom2  6926  pw2f1odclem  6931  opabfi  7035  ctssdccl  7213  omniwomnimkv  7269  nninfwlporlemd  7274  pitric  7434  ltexpi  7450  ltapig  7451  ltmpig  7452  ltanqg  7513  ltmnqg  7514  enq0breq  7549  genpassl  7637  genpassu  7638  1idprl  7703  1idpru  7704  caucvgprlemcanl  7757  ltasrg  7883  prsrlt  7900  caucvgsrlemoffcau  7911  ltpsrprg  7916  map2psrprg  7918  axpre-ltadd  7999  subsub23  8277  leadd1  8503  lemul1  8666  reapmul1lem  8667  reapmul1  8668  reapadd1  8669  apsym  8679  apadd1  8681  apti  8695  apcon4bid  8697  lediv1  8942  lt2mul2div  8952  lerec  8957  ltdiv2  8960  lediv2  8964  le2msq  8974  avgle1  9278  avgle2  9279  nn01to3  9738  qapne  9760  cnref1o  9772  xleneg  9959  xsubge0  10003  xleaddadd  10009  iooneg  10110  iccneg  10111  iccshftr  10116  iccshftl  10118  iccdil  10120  icccntr  10122  fzsplit2  10172  fzaddel  10181  fzrev  10206  elfzo  10271  nelfzo  10274  fzon  10289  elfzom1b  10358  ioo0  10402  ico0  10404  ioc0  10405  flqlt  10426  negqmod0  10476  frec2uzled  10574  expeq0  10715  nn0leexp2  10855  nn0opthlem1d  10865  leisorel  10982  cjreb  11177  ltmininf  11546  minclpr  11548  xrmaxlesup  11570  xrltmininf  11581  xrminltinf  11583  tanaddaplem  12049  nndivdvds  12107  moddvds  12110  modmulconst  12134  oddm1even  12186  ltoddhalfle  12204  bitsp1  12262  dvdssq  12352  phiprmpw  12544  eulerthlemh  12553  odzdvds  12568  pc2dvds  12653  1arith  12690  issubg3  13528  eqgid  13562  resghm2b  13598  conjghm  13612  conjnmzb  13616  ablsubsub23  13661  issrgid  13743  isringid  13787  opprsubgg  13846  opprunitd  13872  crngunit  13873  unitpropdg  13910  issubrng  13961  opprsubrngg  13973  lsslss  14143  lsspropdg  14193  rspsn  14296  znidom  14419  cnrest2  14708  cnptoprest  14711  cnptoprest2  14712  lmss  14718  lmff  14721  txlm  14751  ismet2  14826  blres  14906  xmetec  14909  bdbl  14975  metrest  14978  cnbl0  15006  cnblcld  15007  reopnap  15018  bl2ioo  15022  limcdifap  15134  efle  15248  reapef  15250  logleb  15347  logrpap0b  15348  cxplt  15388  cxple  15389  rpcxple2  15390  rpcxplt2  15391  cxplt3  15392  cxple3  15393  apcxp2  15411  logbleb  15433  logblt  15434  lgsdilem  15504  lgsne0  15515  lgsquadlem1  15554  lgsquadlem2  15555  m1lgs  15562  2lgslem1a  15565  2lgs  15581  iooref1o  15973