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  4742  fvopab3g  5634  respreima  5690  fmptco  5728  cocan1  5834  cocan2  5835  brtposg  6312  nnmword  6576  swoer  6620  erth  6638  brecop  6684  ecopovsymg  6693  xpdom2  6890  pw2f1odclem  6895  opabfi  6999  ctssdccl  7177  omniwomnimkv  7233  nninfwlporlemd  7238  pitric  7388  ltexpi  7404  ltapig  7405  ltmpig  7406  ltanqg  7467  ltmnqg  7468  enq0breq  7503  genpassl  7591  genpassu  7592  1idprl  7657  1idpru  7658  caucvgprlemcanl  7711  ltasrg  7837  prsrlt  7854  caucvgsrlemoffcau  7865  ltpsrprg  7870  map2psrprg  7872  axpre-ltadd  7953  subsub23  8231  leadd1  8457  lemul1  8620  reapmul1lem  8621  reapmul1  8622  reapadd1  8623  apsym  8633  apadd1  8635  apti  8649  apcon4bid  8651  lediv1  8896  lt2mul2div  8906  lerec  8911  ltdiv2  8914  lediv2  8918  le2msq  8928  avgle1  9232  avgle2  9233  nn01to3  9691  qapne  9713  cnref1o  9725  xleneg  9912  xsubge0  9956  xleaddadd  9962  iooneg  10063  iccneg  10064  iccshftr  10069  iccshftl  10071  iccdil  10073  icccntr  10075  fzsplit2  10125  fzaddel  10134  fzrev  10159  elfzo  10224  nelfzo  10227  fzon  10242  elfzom1b  10305  ioo0  10349  ico0  10351  ioc0  10352  flqlt  10373  negqmod0  10423  frec2uzled  10521  expeq0  10662  nn0leexp2  10802  nn0opthlem1d  10812  leisorel  10929  cjreb  11031  ltmininf  11400  minclpr  11402  xrmaxlesup  11424  xrltmininf  11435  xrminltinf  11437  tanaddaplem  11903  nndivdvds  11961  moddvds  11964  modmulconst  11988  oddm1even  12040  ltoddhalfle  12058  bitsp1  12115  dvdssq  12198  phiprmpw  12390  eulerthlemh  12399  odzdvds  12414  pc2dvds  12499  1arith  12536  issubg3  13322  eqgid  13356  resghm2b  13392  conjghm  13406  conjnmzb  13410  ablsubsub23  13455  issrgid  13537  isringid  13581  opprsubgg  13640  opprunitd  13666  crngunit  13667  unitpropdg  13704  issubrng  13755  opprsubrngg  13767  lsslss  13937  lsspropdg  13987  rspsn  14090  znidom  14213  cnrest2  14472  cnptoprest  14475  cnptoprest2  14476  lmss  14482  lmff  14485  txlm  14515  ismet2  14590  blres  14670  xmetec  14673  bdbl  14739  metrest  14742  cnbl0  14770  cnblcld  14771  reopnap  14782  bl2ioo  14786  limcdifap  14898  efle  15012  reapef  15014  logleb  15111  logrpap0b  15112  cxplt  15152  cxple  15153  rpcxple2  15154  rpcxplt2  15155  cxplt3  15156  cxple3  15157  apcxp2  15175  logbleb  15197  logblt  15198  lgsdilem  15268  lgsne0  15279  lgsquadlem1  15318  lgsquadlem2  15319  m1lgs  15326  2lgslem1a  15329  2lgs  15345  iooref1o  15678