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:  ifpdfbidc  991  dfbi3dc  1439  xordidc  1441  19.32dc  1725  r19.32vdc  2680  opbrop  4798  fvopab3g  5709  respreima  5765  fmptco  5803  cocan1  5917  cocan2  5918  brtposg  6406  nnmword  6672  swoer  6716  erth  6734  brecop  6780  ecopovsymg  6789  xpdom2  6998  pw2f1odclem  7003  opabfi  7111  ctssdccl  7289  omniwomnimkv  7345  nninfwlporlemd  7350  pitric  7519  ltexpi  7535  ltapig  7536  ltmpig  7537  ltanqg  7598  ltmnqg  7599  enq0breq  7634  genpassl  7722  genpassu  7723  1idprl  7788  1idpru  7789  caucvgprlemcanl  7842  ltasrg  7968  prsrlt  7985  caucvgsrlemoffcau  7996  ltpsrprg  8001  map2psrprg  8003  axpre-ltadd  8084  subsub23  8362  leadd1  8588  lemul1  8751  reapmul1lem  8752  reapmul1  8753  reapadd1  8754  apsym  8764  apadd1  8766  apti  8780  apcon4bid  8782  lediv1  9027  lt2mul2div  9037  lerec  9042  ltdiv2  9045  lediv2  9049  le2msq  9059  avgle1  9363  avgle2  9364  nn01to3  9824  qapne  9846  cnref1o  9858  xleneg  10045  xsubge0  10089  xleaddadd  10095  iooneg  10196  iccneg  10197  iccshftr  10202  iccshftl  10204  iccdil  10206  icccntr  10208  fzsplit2  10258  fzaddel  10267  fzrev  10292  elfzo  10357  nelfzo  10360  fzon  10375  elfzom1b  10447  ioo0  10491  ico0  10493  ioc0  10494  flqlt  10515  negqmod0  10565  frec2uzled  10663  expeq0  10804  nn0leexp2  10944  nn0opthlem1d  10954  leisorel  11072  cjreb  11392  ltmininf  11761  minclpr  11763  xrmaxlesup  11785  xrltmininf  11796  xrminltinf  11798  tanaddaplem  12264  nndivdvds  12322  moddvds  12325  modmulconst  12349  oddm1even  12401  ltoddhalfle  12419  bitsp1  12477  dvdssq  12567  phiprmpw  12759  eulerthlemh  12768  odzdvds  12783  pc2dvds  12868  1arith  12905  issubg3  13744  eqgid  13778  resghm2b  13814  conjghm  13828  conjnmzb  13832  ablsubsub23  13877  issrgid  13959  isringid  14003  opprsubgg  14062  opprunitd  14089  crngunit  14090  unitpropdg  14127  issubrng  14178  opprsubrngg  14190  lsslss  14360  lsspropdg  14410  rspsn  14513  znidom  14636  cnrest2  14925  cnptoprest  14928  cnptoprest2  14929  lmss  14935  lmff  14938  txlm  14968  ismet2  15043  blres  15123  xmetec  15126  bdbl  15192  metrest  15195  cnbl0  15223  cnblcld  15224  reopnap  15235  bl2ioo  15239  limcdifap  15351  efle  15465  reapef  15467  logleb  15564  logrpap0b  15565  cxplt  15605  cxple  15606  rpcxple2  15607  rpcxplt2  15608  cxplt3  15609  cxple3  15610  apcxp2  15628  logbleb  15650  logblt  15651  lgsdilem  15721  lgsne0  15732  lgsquadlem1  15771  lgsquadlem2  15772  m1lgs  15779  2lgslem1a  15782  2lgs  15798  ausgrusgrben  15981  uspgr2wlkeq  16106  iooref1o  16462