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  1416  xordidc  1418  19.32dc  1701  r19.32vdc  2654  opbrop  4753  fvopab3g  5651  respreima  5707  fmptco  5745  cocan1  5855  cocan2  5856  brtposg  6339  nnmword  6603  swoer  6647  erth  6665  brecop  6711  ecopovsymg  6720  xpdom2  6925  pw2f1odclem  6930  opabfi  7034  ctssdccl  7212  omniwomnimkv  7268  nninfwlporlemd  7273  pitric  7433  ltexpi  7449  ltapig  7450  ltmpig  7451  ltanqg  7512  ltmnqg  7513  enq0breq  7548  genpassl  7636  genpassu  7637  1idprl  7702  1idpru  7703  caucvgprlemcanl  7756  ltasrg  7882  prsrlt  7899  caucvgsrlemoffcau  7910  ltpsrprg  7915  map2psrprg  7917  axpre-ltadd  7998  subsub23  8276  leadd1  8502  lemul1  8665  reapmul1lem  8666  reapmul1  8667  reapadd1  8668  apsym  8678  apadd1  8680  apti  8694  apcon4bid  8696  lediv1  8941  lt2mul2div  8951  lerec  8956  ltdiv2  8959  lediv2  8963  le2msq  8973  avgle1  9277  avgle2  9278  nn01to3  9737  qapne  9759  cnref1o  9771  xleneg  9958  xsubge0  10002  xleaddadd  10008  iooneg  10109  iccneg  10110  iccshftr  10115  iccshftl  10117  iccdil  10119  icccntr  10121  fzsplit2  10171  fzaddel  10180  fzrev  10205  elfzo  10270  nelfzo  10273  fzon  10288  elfzom1b  10356  ioo0  10400  ico0  10402  ioc0  10403  flqlt  10424  negqmod0  10474  frec2uzled  10572  expeq0  10713  nn0leexp2  10853  nn0opthlem1d  10863  leisorel  10980  cjreb  11148  ltmininf  11517  minclpr  11519  xrmaxlesup  11541  xrltmininf  11552  xrminltinf  11554  tanaddaplem  12020  nndivdvds  12078  moddvds  12081  modmulconst  12105  oddm1even  12157  ltoddhalfle  12175  bitsp1  12233  dvdssq  12323  phiprmpw  12515  eulerthlemh  12524  odzdvds  12539  pc2dvds  12624  1arith  12661  issubg3  13499  eqgid  13533  resghm2b  13569  conjghm  13583  conjnmzb  13587  ablsubsub23  13632  issrgid  13714  isringid  13758  opprsubgg  13817  opprunitd  13843  crngunit  13844  unitpropdg  13881  issubrng  13932  opprsubrngg  13944  lsslss  14114  lsspropdg  14164  rspsn  14267  znidom  14390  cnrest2  14679  cnptoprest  14682  cnptoprest2  14683  lmss  14689  lmff  14692  txlm  14722  ismet2  14797  blres  14877  xmetec  14880  bdbl  14946  metrest  14949  cnbl0  14977  cnblcld  14978  reopnap  14989  bl2ioo  14993  limcdifap  15105  efle  15219  reapef  15221  logleb  15318  logrpap0b  15319  cxplt  15359  cxple  15360  rpcxple2  15361  rpcxplt2  15362  cxplt3  15363  cxple3  15364  apcxp2  15382  logbleb  15404  logblt  15405  lgsdilem  15475  lgsne0  15486  lgsquadlem1  15525  lgsquadlem2  15526  m1lgs  15533  2lgslem1a  15536  2lgs  15552  iooref1o  15935