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:  ifpdfbidc  994  dfbi3dc  1442  xordidc  1444  19.32dc  1727  r19.32vdc  2694  opbrop  4834  fvopab3g  5755  respreima  5810  fmptco  5848  cocan1  5966  cocan2  5967  suppimacnvfn  6459  brtposg  6498  nnmword  6764  swoer  6808  erth  6826  brecop  6872  ecopovsymg  6881  xpdom2  7095  pw2f1odclem  7100  opabfi  7213  ctssdccl  7415  omniwomnimkv  7471  nninfwlporlemd  7476  pitric  7652  ltexpi  7668  ltapig  7669  ltmpig  7670  ltanqg  7731  ltmnqg  7732  enq0breq  7767  genpassl  7855  genpassu  7856  1idprl  7921  1idpru  7922  caucvgprlemcanl  7975  ltasrg  8101  prsrlt  8118  caucvgsrlemoffcau  8129  ltpsrprg  8134  map2psrprg  8136  axpre-ltadd  8217  subsub23  8494  leadd1  8721  lemul1  8884  reapmul1lem  8885  reapmul1  8886  reapadd1  8887  apsym  8897  apadd1  8899  apti  8913  apcon4bid  8915  lediv1  9160  lt2mul2div  9170  lerec  9175  ltdiv2  9178  lediv2  9182  le2msq  9192  avgle1  9496  avgle2  9497  nn01to3  9967  qapne  9989  cnref1o  10001  xleneg  10189  xsubge0  10233  xleaddadd  10239  iooneg  10340  iccneg  10341  iccshftr  10346  iccshftl  10348  iccdil  10350  icccntr  10352  fzsplit2  10404  fzaddel  10414  fzrev  10440  elfzo  10505  nelfzo  10508  fzon  10523  elfzom1b  10596  ioo0  10643  ico0  10645  ioc0  10646  flqlt  10667  negqmod0  10717  frec2uzled  10815  expeq0  10956  nn0leexp2  11097  nn0opthlem1d  11107  leisorel  11234  cjreb  11576  ltmininf  11945  minclpr  11947  xrmaxlesup  11969  xrltmininf  11980  xrminltinf  11982  tanaddaplem  12449  nndivdvds  12507  moddvds  12510  modmulconst  12534  oddm1even  12586  ltoddhalfle  12604  bitsp1  12662  dvdssq  12752  phiprmpw  12944  eulerthlemh  12953  odzdvds  12968  pc2dvds  13053  1arith  13090  issubg3  13945  eqgid  13979  resghm2b  14015  conjghm  14029  conjnmzb  14033  ablsubsub23  14078  issrgid  14224  isringid  14268  opprsubgg  14328  opprunitd  14355  crngunit  14356  unitpropdg  14393  issubrng  14445  opprsubrngg  14457  opprdrng  14558  lsslss  14655  lsspropdg  14705  rspsn  14808  znidom  14931  psrbagconf1o  14954  cnrest2  15227  cnptoprest  15230  cnptoprest2  15231  lmss  15237  lmff  15240  txlm  15270  ismet2  15345  blres  15425  xmetec  15428  bdbl  15494  metrest  15497  cnbl0  15525  cnblcld  15526  reopnap  15537  bl2ioo  15541  limcdifap  15653  efle  15767  reapef  15769  logleb  15866  logrpap0b  15867  cxplt  15907  cxple  15908  rpcxple2  15909  rpcxplt2  15910  cxplt3  15911  cxple3  15912  apcxp2  15930  logbleb  15952  logblt  15953  lgsdilem  16026  lgsne0  16037  lgsquadlem1  16076  lgsquadlem2  16077  m1lgs  16084  2lgslem1a  16087  2lgs  16103  ausgrusgrben  16289  uspgr2wlkeq  16486  isclwwlknx  16537  eupth2lem3lem6fi  16592  iooref1o  16944