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  2683  opbrop  4811  fvopab3g  5728  respreima  5783  fmptco  5821  cocan1  5938  cocan2  5939  suppimacnvfn  6424  brtposg  6463  nnmword  6729  swoer  6773  erth  6791  brecop  6837  ecopovsymg  6846  xpdom2  7058  pw2f1odclem  7063  opabfi  7175  ctssdccl  7353  omniwomnimkv  7409  nninfwlporlemd  7414  pitric  7584  ltexpi  7600  ltapig  7601  ltmpig  7602  ltanqg  7663  ltmnqg  7664  enq0breq  7699  genpassl  7787  genpassu  7788  1idprl  7853  1idpru  7854  caucvgprlemcanl  7907  ltasrg  8033  prsrlt  8050  caucvgsrlemoffcau  8061  ltpsrprg  8066  map2psrprg  8068  axpre-ltadd  8149  subsub23  8426  leadd1  8652  lemul1  8815  reapmul1lem  8816  reapmul1  8817  reapadd1  8818  apsym  8828  apadd1  8830  apti  8844  apcon4bid  8846  lediv1  9091  lt2mul2div  9101  lerec  9106  ltdiv2  9109  lediv2  9113  le2msq  9123  avgle1  9427  avgle2  9428  nn01to3  9895  qapne  9917  cnref1o  9929  xleneg  10116  xsubge0  10160  xleaddadd  10166  iooneg  10267  iccneg  10268  iccshftr  10273  iccshftl  10275  iccdil  10277  icccntr  10279  fzsplit2  10330  fzaddel  10339  fzrev  10364  elfzo  10429  nelfzo  10432  fzon  10447  elfzom1b  10520  ioo0  10565  ico0  10567  ioc0  10568  flqlt  10589  negqmod0  10639  frec2uzled  10737  expeq0  10878  nn0leexp2  11018  nn0opthlem1d  11028  leisorel  11147  cjreb  11489  ltmininf  11858  minclpr  11860  xrmaxlesup  11882  xrltmininf  11893  xrminltinf  11895  tanaddaplem  12362  nndivdvds  12420  moddvds  12423  modmulconst  12447  oddm1even  12499  ltoddhalfle  12517  bitsp1  12575  dvdssq  12665  phiprmpw  12857  eulerthlemh  12866  odzdvds  12881  pc2dvds  12966  1arith  13003  issubg3  13842  eqgid  13876  resghm2b  13912  conjghm  13926  conjnmzb  13930  ablsubsub23  13975  issrgid  14058  isringid  14102  opprsubgg  14161  opprunitd  14188  crngunit  14189  unitpropdg  14226  issubrng  14277  opprsubrngg  14289  lsslss  14460  lsspropdg  14510  rspsn  14613  znidom  14736  psrbagconf1o  14757  cnrest2  15030  cnptoprest  15033  cnptoprest2  15034  lmss  15040  lmff  15043  txlm  15073  ismet2  15148  blres  15228  xmetec  15231  bdbl  15297  metrest  15300  cnbl0  15328  cnblcld  15329  reopnap  15340  bl2ioo  15344  limcdifap  15456  efle  15570  reapef  15572  logleb  15669  logrpap0b  15670  cxplt  15710  cxple  15711  rpcxple2  15712  rpcxplt2  15713  cxplt3  15714  cxple3  15715  apcxp2  15733  logbleb  15755  logblt  15756  lgsdilem  15829  lgsne0  15840  lgsquadlem1  15879  lgsquadlem2  15880  m1lgs  15887  2lgslem1a  15890  2lgs  15906  ausgrusgrben  16092  uspgr2wlkeq  16289  isclwwlknx  16340  eupth2lem3lem6fi  16395  iooref1o  16749