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  1408  xordidc  1410  19.32dc  1693  r19.32vdc  2646  opbrop  4743  fvopab3g  5637  respreima  5693  fmptco  5731  cocan1  5837  cocan2  5838  brtposg  6321  nnmword  6585  swoer  6629  erth  6647  brecop  6693  ecopovsymg  6702  xpdom2  6899  pw2f1odclem  6904  opabfi  7008  ctssdccl  7186  omniwomnimkv  7242  nninfwlporlemd  7247  pitric  7405  ltexpi  7421  ltapig  7422  ltmpig  7423  ltanqg  7484  ltmnqg  7485  enq0breq  7520  genpassl  7608  genpassu  7609  1idprl  7674  1idpru  7675  caucvgprlemcanl  7728  ltasrg  7854  prsrlt  7871  caucvgsrlemoffcau  7882  ltpsrprg  7887  map2psrprg  7889  axpre-ltadd  7970  subsub23  8248  leadd1  8474  lemul1  8637  reapmul1lem  8638  reapmul1  8639  reapadd1  8640  apsym  8650  apadd1  8652  apti  8666  apcon4bid  8668  lediv1  8913  lt2mul2div  8923  lerec  8928  ltdiv2  8931  lediv2  8935  le2msq  8945  avgle1  9249  avgle2  9250  nn01to3  9708  qapne  9730  cnref1o  9742  xleneg  9929  xsubge0  9973  xleaddadd  9979  iooneg  10080  iccneg  10081  iccshftr  10086  iccshftl  10088  iccdil  10090  icccntr  10092  fzsplit2  10142  fzaddel  10151  fzrev  10176  elfzo  10241  nelfzo  10244  fzon  10259  elfzom1b  10322  ioo0  10366  ico0  10368  ioc0  10369  flqlt  10390  negqmod0  10440  frec2uzled  10538  expeq0  10679  nn0leexp2  10819  nn0opthlem1d  10829  leisorel  10946  cjreb  11048  ltmininf  11417  minclpr  11419  xrmaxlesup  11441  xrltmininf  11452  xrminltinf  11454  tanaddaplem  11920  nndivdvds  11978  moddvds  11981  modmulconst  12005  oddm1even  12057  ltoddhalfle  12075  bitsp1  12133  dvdssq  12223  phiprmpw  12415  eulerthlemh  12424  odzdvds  12439  pc2dvds  12524  1arith  12561  issubg3  13398  eqgid  13432  resghm2b  13468  conjghm  13482  conjnmzb  13486  ablsubsub23  13531  issrgid  13613  isringid  13657  opprsubgg  13716  opprunitd  13742  crngunit  13743  unitpropdg  13780  issubrng  13831  opprsubrngg  13843  lsslss  14013  lsspropdg  14063  rspsn  14166  znidom  14289  cnrest2  14556  cnptoprest  14559  cnptoprest2  14560  lmss  14566  lmff  14569  txlm  14599  ismet2  14674  blres  14754  xmetec  14757  bdbl  14823  metrest  14826  cnbl0  14854  cnblcld  14855  reopnap  14866  bl2ioo  14870  limcdifap  14982  efle  15096  reapef  15098  logleb  15195  logrpap0b  15196  cxplt  15236  cxple  15237  rpcxple2  15238  rpcxplt2  15239  cxplt3  15240  cxple3  15241  apcxp2  15259  logbleb  15281  logblt  15282  lgsdilem  15352  lgsne0  15363  lgsquadlem1  15402  lgsquadlem2  15403  m1lgs  15410  2lgslem1a  15413  2lgs  15429  iooref1o  15765