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  993  dfbi3dc  1441  xordidc  1443  19.32dc  1727  r19.32vdc  2682  opbrop  4805  fvopab3g  5719  respreima  5775  fmptco  5813  cocan1  5927  cocan2  5928  brtposg  6419  nnmword  6685  swoer  6729  erth  6747  brecop  6793  ecopovsymg  6802  xpdom2  7014  pw2f1odclem  7019  opabfi  7131  ctssdccl  7309  omniwomnimkv  7365  nninfwlporlemd  7370  pitric  7540  ltexpi  7556  ltapig  7557  ltmpig  7558  ltanqg  7619  ltmnqg  7620  enq0breq  7655  genpassl  7743  genpassu  7744  1idprl  7809  1idpru  7810  caucvgprlemcanl  7863  ltasrg  7989  prsrlt  8006  caucvgsrlemoffcau  8017  ltpsrprg  8022  map2psrprg  8024  axpre-ltadd  8105  subsub23  8383  leadd1  8609  lemul1  8772  reapmul1lem  8773  reapmul1  8774  reapadd1  8775  apsym  8785  apadd1  8787  apti  8801  apcon4bid  8803  lediv1  9048  lt2mul2div  9058  lerec  9063  ltdiv2  9066  lediv2  9070  le2msq  9080  avgle1  9384  avgle2  9385  nn01to3  9850  qapne  9872  cnref1o  9884  xleneg  10071  xsubge0  10115  xleaddadd  10121  iooneg  10222  iccneg  10223  iccshftr  10228  iccshftl  10230  iccdil  10232  icccntr  10234  fzsplit2  10284  fzaddel  10293  fzrev  10318  elfzo  10383  nelfzo  10386  fzon  10401  elfzom1b  10473  ioo0  10518  ico0  10520  ioc0  10521  flqlt  10542  negqmod0  10592  frec2uzled  10690  expeq0  10831  nn0leexp2  10971  nn0opthlem1d  10981  leisorel  11100  cjreb  11426  ltmininf  11795  minclpr  11797  xrmaxlesup  11819  xrltmininf  11830  xrminltinf  11832  tanaddaplem  12298  nndivdvds  12356  moddvds  12359  modmulconst  12383  oddm1even  12435  ltoddhalfle  12453  bitsp1  12511  dvdssq  12601  phiprmpw  12793  eulerthlemh  12802  odzdvds  12817  pc2dvds  12902  1arith  12939  issubg3  13778  eqgid  13812  resghm2b  13848  conjghm  13862  conjnmzb  13866  ablsubsub23  13911  issrgid  13993  isringid  14037  opprsubgg  14096  opprunitd  14123  crngunit  14124  unitpropdg  14161  issubrng  14212  opprsubrngg  14224  lsslss  14394  lsspropdg  14444  rspsn  14547  znidom  14670  cnrest2  14959  cnptoprest  14962  cnptoprest2  14963  lmss  14969  lmff  14972  txlm  15002  ismet2  15077  blres  15157  xmetec  15160  bdbl  15226  metrest  15229  cnbl0  15257  cnblcld  15258  reopnap  15269  bl2ioo  15273  limcdifap  15385  efle  15499  reapef  15501  logleb  15598  logrpap0b  15599  cxplt  15639  cxple  15640  rpcxple2  15641  rpcxplt2  15642  cxplt3  15643  cxple3  15644  apcxp2  15662  logbleb  15684  logblt  15685  lgsdilem  15755  lgsne0  15766  lgsquadlem1  15805  lgsquadlem2  15806  m1lgs  15813  2lgslem1a  15816  2lgs  15832  ausgrusgrben  16018  uspgr2wlkeq  16215  isclwwlknx  16266  iooref1o  16638