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  2692  opbrop  4829  fvopab3g  5750  respreima  5805  fmptco  5843  cocan1  5960  cocan2  5961  suppimacnvfn  6446  brtposg  6485  nnmword  6751  swoer  6795  erth  6813  brecop  6859  ecopovsymg  6868  xpdom2  7082  pw2f1odclem  7087  opabfi  7200  ctssdccl  7402  omniwomnimkv  7458  nninfwlporlemd  7463  pitric  7636  ltexpi  7652  ltapig  7653  ltmpig  7654  ltanqg  7715  ltmnqg  7716  enq0breq  7751  genpassl  7839  genpassu  7840  1idprl  7905  1idpru  7906  caucvgprlemcanl  7959  ltasrg  8085  prsrlt  8102  caucvgsrlemoffcau  8113  ltpsrprg  8118  map2psrprg  8120  axpre-ltadd  8201  subsub23  8478  leadd1  8704  lemul1  8867  reapmul1lem  8868  reapmul1  8869  reapadd1  8870  apsym  8880  apadd1  8882  apti  8896  apcon4bid  8898  lediv1  9143  lt2mul2div  9153  lerec  9158  ltdiv2  9161  lediv2  9165  le2msq  9175  avgle1  9479  avgle2  9480  nn01to3  9949  qapne  9971  cnref1o  9983  xleneg  10170  xsubge0  10214  xleaddadd  10220  iooneg  10321  iccneg  10322  iccshftr  10327  iccshftl  10329  iccdil  10331  icccntr  10333  fzsplit2  10384  fzaddel  10393  fzrev  10418  elfzo  10483  nelfzo  10486  fzon  10501  elfzom1b  10574  ioo0  10619  ico0  10621  ioc0  10622  flqlt  10643  negqmod0  10693  frec2uzled  10791  expeq0  10932  nn0leexp2  11072  nn0opthlem1d  11082  leisorel  11209  cjreb  11551  ltmininf  11920  minclpr  11922  xrmaxlesup  11944  xrltmininf  11955  xrminltinf  11957  tanaddaplem  12424  nndivdvds  12482  moddvds  12485  modmulconst  12509  oddm1even  12561  ltoddhalfle  12579  bitsp1  12637  dvdssq  12727  phiprmpw  12919  eulerthlemh  12928  odzdvds  12943  pc2dvds  13028  1arith  13065  issubg3  13909  eqgid  13943  resghm2b  13979  conjghm  13993  conjnmzb  13997  ablsubsub23  14042  issrgid  14125  isringid  14169  opprsubgg  14228  opprunitd  14255  crngunit  14256  unitpropdg  14293  issubrng  14344  opprsubrngg  14356  lsslss  14529  lsspropdg  14579  rspsn  14682  znidom  14805  psrbagconf1o  14828  cnrest2  15101  cnptoprest  15104  cnptoprest2  15105  lmss  15111  lmff  15114  txlm  15144  ismet2  15219  blres  15299  xmetec  15302  bdbl  15368  metrest  15371  cnbl0  15399  cnblcld  15400  reopnap  15411  bl2ioo  15415  limcdifap  15527  efle  15641  reapef  15643  logleb  15740  logrpap0b  15741  cxplt  15781  cxple  15782  rpcxple2  15783  rpcxplt2  15784  cxplt3  15785  cxple3  15786  apcxp2  15804  logbleb  15826  logblt  15827  lgsdilem  15900  lgsne0  15911  lgsquadlem1  15950  lgsquadlem2  15951  m1lgs  15958  2lgslem1a  15961  2lgs  15977  ausgrusgrben  16163  uspgr2wlkeq  16360  isclwwlknx  16411  eupth2lem3lem6fi  16466  iooref1o  16818