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  14048  eqgid  14082  resghm2b  14118  conjghm  14132  conjnmzb  14136  resscntz  14160  cntzrec  14163  ablsubsub23  14213  issrgid  14369  isringid  14414  opprsubgg  14474  opprunitd  14501  crngunit  14502  unitpropdg  14539  issubrng  14591  opprsubrngg  14603  opprdrng  14704  lsslss  14802  lsspropdg  14852  rspsn  14955  znidom  15076  psrbagconf1o  15149  cnrest2  15428  cnptoprest  15431  cnptoprest2  15432  lmss  15438  lmff  15441  txlm  15471  ismet2  15546  blres  15626  xmetec  15629  bdbl  15695  metrest  15698  cnbl0  15726  cnblcld  15727  reopnap  15738  bl2ioo  15742  limcdifap  15854  efle  15968  reapef  15970  logleb  16069  logrpap0b  16070  logdivle  16089  cxplt  16113  cxple  16114  rpcxple2  16115  rpcxplt2  16116  cxplt3  16117  cxple3  16118  apcxp2  16136  logbleb  16158  logblt  16159  lgsdilem  16312  lgsne0  16323  lgsquadlem1  16362  lgsquadlem2  16363  m1lgs  16370  2lgslem1a  16373  2lgs  16389  ausgrusgrben  16575  uspgr2wlkeq  16772  isclwwlknx  16823  eupth2lem3lem6fi  16878  iooref1o  17249