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  1397  xordidc  1399  19.32dc  1679  r19.32vdc  2626  opbrop  4703  fvopab3g  5586  respreima  5641  fmptco  5679  cocan1  5783  cocan2  5784  brtposg  6250  nnmword  6514  swoer  6558  erth  6574  brecop  6620  ecopovsymg  6629  xpdom2  6826  ctssdccl  7105  omniwomnimkv  7160  nninfwlporlemd  7165  pitric  7315  ltexpi  7331  ltapig  7332  ltmpig  7333  ltanqg  7394  ltmnqg  7395  enq0breq  7430  genpassl  7518  genpassu  7519  1idprl  7584  1idpru  7585  caucvgprlemcanl  7638  ltasrg  7764  prsrlt  7781  caucvgsrlemoffcau  7792  ltpsrprg  7797  map2psrprg  7799  axpre-ltadd  7880  subsub23  8156  leadd1  8381  lemul1  8544  reapmul1lem  8545  reapmul1  8546  reapadd1  8547  apsym  8557  apadd1  8559  apti  8573  apcon4bid  8575  lediv1  8820  lt2mul2div  8830  lerec  8835  ltdiv2  8838  lediv2  8842  le2msq  8852  avgle1  9153  avgle2  9154  nn01to3  9611  qapne  9633  cnref1o  9644  xleneg  9831  xsubge0  9875  xleaddadd  9881  iooneg  9982  iccneg  9983  iccshftr  9988  iccshftl  9990  iccdil  9992  icccntr  9994  fzsplit2  10043  fzaddel  10052  fzrev  10077  elfzo  10142  fzon  10159  elfzom1b  10222  ioo0  10253  ico0  10255  ioc0  10256  flqlt  10276  negqmod0  10324  frec2uzled  10422  expeq0  10544  nn0leexp2  10682  nn0opthlem1d  10691  leisorel  10808  cjreb  10866  ltmininf  11234  minclpr  11236  xrmaxlesup  11258  xrltmininf  11269  xrminltinf  11271  tanaddaplem  11737  nndivdvds  11794  moddvds  11797  modmulconst  11821  oddm1even  11870  ltoddhalfle  11888  dvdssq  12022  phiprmpw  12212  eulerthlemh  12221  odzdvds  12235  pc2dvds  12319  1arith  12355  issubg3  12978  ablsubsub23  13028  issrgid  13064  isringid  13108  opprunitd  13178  crngunit  13179  unitpropdg  13216  cnrest2  13518  cnptoprest  13521  cnptoprest2  13522  lmss  13528  lmff  13531  txlm  13561  ismet2  13636  blres  13716  xmetec  13719  bdbl  13785  metrest  13788  cnbl0  13816  cnblcld  13817  reopnap  13820  bl2ioo  13824  limcdifap  13913  efle  13979  reapef  13981  logleb  14078  logrpap0b  14079  cxplt  14118  cxple  14119  rpcxple2  14120  rpcxplt2  14121  cxplt3  14122  cxple3  14123  apcxp2  14140  logbleb  14161  logblt  14162  lgsdilem  14210  lgsne0  14221  iooref1o  14553