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 ) )

This proof depends on syntax axioms:   -> wi 4   <-> wb 105

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117

This theorem is used by:  ifpdfbidc  998  dfbi3dc  1446  xordidc  1448  19.32dc  1731  r19.32vdc  2700  opbrop  4856  fvopab3g  5781  respreima  5839  fmptco  5877  cocan1  5996  cocan2  5997  suppimacnvfn  6490  suppinisegdc  6513  brtposg  6530  nnmword  6796  swoer  6840  erth  6858  brecop  6904  ecopovsymg  6913  xpdom2  7135  pw2f1odclem  7140  opabfi  7253  ctssdccl  7457  omniwomnimkv  7513  nninfwlporlemd  7518  pitric  7694  ltexpi  7710  ltapig  7711  ltmpig  7712  ltanqg  7773  ltmnqg  7774  enq0breq  7809  genpassl  7897  genpassu  7898  1idprl  7963  1idpru  7964  caucvgprlemcanl  8017  ltasrg  8143  prsrlt  8160  caucvgsrlemoffcau  8171  ltpsrprg  8176  map2psrprg  8178  axpre-ltadd  8259  subsub23  8538  leadd1  8765  lemul1  8929  reapmul1lem  8930  reapmul1  8931  reapadd1  8932  apsym  8942  apadd1  8944  apti  8958  apcon4bid  8960  lediv1  9207  lt2mul2div  9217  lerec  9222  ltdiv2  9225  lediv2  9229  le2msq  9239  ofsubeq0  9300  avgle1  9557  avgle2  9558  nn01to3  10032  qapne  10054  cnref1o  10067  xleneg  10255  xsubge0  10299  xleaddadd  10305  iooneg  10406  iccneg  10407  iccshftr  10412  iccshftl  10414  iccdil  10416  icccntr  10418  fzsplit2  10471  fzaddel  10481  fzrev  10507  elfzo  10572  nelfzo  10575  fzon  10590  elfzom1b  10663  ioo0  10710  ico0  10712  ioc0  10713  flqlt  10737  negqmod0  10788  frec2uzled  10886  expeq0  11027  nn0leexp2  11169  nn0opthlem1d  11179  leisorel  11310  cjreb  11652  ltmininf  12024  minclpr  12026  xrmaxlesup  12049  xrltmininf  12060  xrminltinf  12062  tanaddaplem  12529  nndivdvds  12587  moddvds  12590  modmulconst  12614  oddm1even  12666  ltoddhalfle  12684  bitsp1  12742  dvdssq  12832  phiprmpw  13028  eulerthlemh  13037  odzdvds  13052  pc2dvds  13137  1arith  13174  issubg3  14053  eqgid  14087  resghm2b  14123  conjghm  14137  conjnmzb  14141  resscntz  14165  cntzrec  14168  ablsubsub23  14218  issrgid  14391  isringid  14436  opprsubgg  14498  opprunitd  14525  crngunit  14526  unitpropdg  14563  issubrng  14615  opprsubrngg  14627  opprdrng  14728  lsslss  14826  lsspropdg  14876  rspsn  14979  znidom  15100  psrbagconf1o  15177  gsumbagdiaglem  15184  cnrest2  15479  cnptoprest  15482  cnptoprest2  15483  lmss  15489  lmff  15492  txlm  15522  ismet2  15597  blres  15677  xmetec  15680  bdbl  15746  metrest  15749  cnbl0  15777  cnblcld  15778  reopnap  15789  bl2ioo  15793  limcdifap  15905  efle  16019  reapef  16021  logleb  16122  logrpap0b  16123  logdivle  16142  cxplt  16168  cxple  16169  rpcxple2  16170  rpcxplt2  16171  cxplt3  16172  cxple3  16173  apcxp2  16191  logbleb  16214  logblt  16215  lgsdilem  16368  lgsne0  16379  lgsquadlem1  16418  lgsquadlem2  16419  m1lgs  16426  2lgslem1a  16429  2lgs  16445  ausgrusgrben  16631  uspgr2wlkeq  16828  isclwwlknx  16879  eupth2lem3lem6fi  16934  iooref1o  17306