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  4854  fvopab3g  5778  respreima  5836  fmptco  5874  cocan1  5993  cocan2  5994  suppimacnvfn  6486  brtposg  6525  nnmword  6791  swoer  6835  erth  6853  brecop  6899  ecopovsymg  6908  xpdom2  7129  pw2f1odclem  7134  opabfi  7247  ctssdccl  7452  omniwomnimkv  7508  nninfwlporlemd  7513  pitric  7689  ltexpi  7705  ltapig  7706  ltmpig  7707  ltanqg  7768  ltmnqg  7769  enq0breq  7804  genpassl  7892  genpassu  7893  1idprl  7958  1idpru  7959  caucvgprlemcanl  8012  ltasrg  8138  prsrlt  8155  caucvgsrlemoffcau  8166  ltpsrprg  8171  map2psrprg  8173  axpre-ltadd  8254  subsub23  8533  leadd1  8760  lemul1  8924  reapmul1lem  8925  reapmul1  8926  reapadd1  8927  apsym  8937  apadd1  8939  apti  8953  apcon4bid  8955  lediv1  9202  lt2mul2div  9212  lerec  9217  ltdiv2  9220  lediv2  9224  le2msq  9234  avgle1  9551  avgle2  9552  nn01to3  10027  qapne  10049  cnref1o  10062  xleneg  10250  xsubge0  10294  xleaddadd  10300  iooneg  10401  iccneg  10402  iccshftr  10407  iccshftl  10409  iccdil  10411  icccntr  10413  fzsplit2  10466  fzaddel  10476  fzrev  10502  elfzo  10567  nelfzo  10570  fzon  10585  elfzom1b  10658  ioo0  10705  ico0  10707  ioc0  10708  flqlt  10732  negqmod0  10783  frec2uzled  10881  expeq0  11022  nn0leexp2  11164  nn0opthlem1d  11174  leisorel  11305  cjreb  11647  ltmininf  12019  minclpr  12021  xrmaxlesup  12044  xrltmininf  12055  xrminltinf  12057  tanaddaplem  12524  nndivdvds  12582  moddvds  12585  modmulconst  12609  oddm1even  12661  ltoddhalfle  12679  bitsp1  12737  dvdssq  12827  phiprmpw  13023  eulerthlemh  13032  odzdvds  13047  pc2dvds  13132  1arith  13169  issubg3  14047  eqgid  14081  resghm2b  14117  conjghm  14131  conjnmzb  14135  ablsubsub23  14181  issrgid  14337  isringid  14382  opprsubgg  14442  opprunitd  14469  crngunit  14470  unitpropdg  14507  issubrng  14559  opprsubrngg  14571  opprdrng  14672  lsslss  14770  lsspropdg  14820  rspsn  14923  znidom  15044  psrbagconf1o  15117  cnrest2  15390  cnptoprest  15393  cnptoprest2  15394  lmss  15400  lmff  15403  txlm  15433  ismet2  15508  blres  15588  xmetec  15591  bdbl  15657  metrest  15660  cnbl0  15688  cnblcld  15689  reopnap  15700  bl2ioo  15704  limcdifap  15816  efle  15930  reapef  15932  logleb  16031  logrpap0b  16032  logdivle  16051  cxplt  16075  cxple  16076  rpcxple2  16077  rpcxplt2  16078  cxplt3  16079  cxple3  16080  apcxp2  16098  logbleb  16120  logblt  16121  lgsdilem  16274  lgsne0  16285  lgsquadlem1  16324  lgsquadlem2  16325  m1lgs  16332  2lgslem1a  16335  2lgs  16351  ausgrusgrben  16537  uspgr2wlkeq  16734  isclwwlknx  16785  eupth2lem3lem6fi  16840  iooref1o  17211