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  1690  r19.32vdc  2639  opbrop  4723  fvopab3g  5610  respreima  5665  fmptco  5703  cocan1  5809  cocan2  5810  brtposg  6280  nnmword  6544  swoer  6588  erth  6606  brecop  6652  ecopovsymg  6661  xpdom2  6858  pw2f1odclem  6863  ctssdccl  7141  omniwomnimkv  7196  nninfwlporlemd  7201  pitric  7351  ltexpi  7367  ltapig  7368  ltmpig  7369  ltanqg  7430  ltmnqg  7431  enq0breq  7466  genpassl  7554  genpassu  7555  1idprl  7620  1idpru  7621  caucvgprlemcanl  7674  ltasrg  7800  prsrlt  7817  caucvgsrlemoffcau  7828  ltpsrprg  7833  map2psrprg  7835  axpre-ltadd  7916  subsub23  8193  leadd1  8418  lemul1  8581  reapmul1lem  8582  reapmul1  8583  reapadd1  8584  apsym  8594  apadd1  8596  apti  8610  apcon4bid  8612  lediv1  8857  lt2mul2div  8867  lerec  8872  ltdiv2  8875  lediv2  8879  le2msq  8889  avgle1  9190  avgle2  9191  nn01to3  9649  qapne  9671  cnref1o  9682  xleneg  9869  xsubge0  9913  xleaddadd  9919  iooneg  10020  iccneg  10021  iccshftr  10026  iccshftl  10028  iccdil  10030  icccntr  10032  fzsplit2  10082  fzaddel  10091  fzrev  10116  elfzo  10181  fzon  10198  elfzom1b  10261  ioo0  10292  ico0  10294  ioc0  10295  flqlt  10316  negqmod0  10364  frec2uzled  10462  expeq0  10585  nn0leexp2  10725  nn0opthlem1d  10735  leisorel  10852  cjreb  10910  ltmininf  11278  minclpr  11280  xrmaxlesup  11302  xrltmininf  11313  xrminltinf  11315  tanaddaplem  11781  nndivdvds  11838  moddvds  11841  modmulconst  11865  oddm1even  11915  ltoddhalfle  11933  dvdssq  12067  phiprmpw  12257  eulerthlemh  12266  odzdvds  12280  pc2dvds  12365  1arith  12402  issubg3  13148  eqgid  13182  resghm2b  13218  conjghm  13232  conjnmzb  13236  ablsubsub23  13281  issrgid  13352  isringid  13396  opprsubgg  13451  opprunitd  13477  crngunit  13478  unitpropdg  13515  issubrng  13563  opprsubrngg  13575  lsslss  13714  lsspropdg  13764  cnrest2  14213  cnptoprest  14216  cnptoprest2  14217  lmss  14223  lmff  14226  txlm  14256  ismet2  14331  blres  14411  xmetec  14414  bdbl  14480  metrest  14483  cnbl0  14511  cnblcld  14512  reopnap  14515  bl2ioo  14519  limcdifap  14608  efle  14674  reapef  14676  logleb  14773  logrpap0b  14774  cxplt  14813  cxple  14814  rpcxple2  14815  rpcxplt2  14816  cxplt3  14817  cxple3  14818  apcxp2  14835  logbleb  14856  logblt  14857  lgsdilem  14906  lgsne0  14917  m1lgs  14930  iooref1o  15261