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  998  dfbi3dc  1446  xordidc  1448  19.32dc  1731  r19.32vdc  2700  opbrop  4849  fvopab3g  5772  respreima  5827  fmptco  5865  cocan1  5983  cocan2  5984  suppimacnvfn  6476  brtposg  6515  nnmword  6781  swoer  6825  erth  6843  brecop  6889  ecopovsymg  6898  xpdom2  7119  pw2f1odclem  7124  opabfi  7237  ctssdccl  7441  omniwomnimkv  7497  nninfwlporlemd  7502  pitric  7678  ltexpi  7694  ltapig  7695  ltmpig  7696  ltanqg  7757  ltmnqg  7758  enq0breq  7793  genpassl  7881  genpassu  7882  1idprl  7947  1idpru  7948  caucvgprlemcanl  8001  ltasrg  8127  prsrlt  8144  caucvgsrlemoffcau  8155  ltpsrprg  8160  map2psrprg  8162  axpre-ltadd  8243  subsub23  8521  leadd1  8748  lemul1  8911  reapmul1lem  8912  reapmul1  8913  reapadd1  8914  apsym  8924  apadd1  8926  apti  8940  apcon4bid  8942  lediv1  9189  lt2mul2div  9199  lerec  9204  ltdiv2  9207  lediv2  9211  le2msq  9221  avgle1  9525  avgle2  9526  nn01to3  9996  qapne  10018  cnref1o  10030  xleneg  10218  xsubge0  10262  xleaddadd  10268  iooneg  10369  iccneg  10370  iccshftr  10375  iccshftl  10377  iccdil  10379  icccntr  10381  fzsplit2  10433  fzaddel  10443  fzrev  10469  elfzo  10534  nelfzo  10537  fzon  10552  elfzom1b  10625  ioo0  10672  ico0  10674  ioc0  10675  flqlt  10696  negqmod0  10746  frec2uzled  10844  expeq0  10985  nn0leexp2  11126  nn0opthlem1d  11136  leisorel  11267  cjreb  11609  ltmininf  11979  minclpr  11981  xrmaxlesup  12003  xrltmininf  12014  xrminltinf  12016  tanaddaplem  12483  nndivdvds  12541  moddvds  12544  modmulconst  12568  oddm1even  12620  ltoddhalfle  12638  bitsp1  12696  dvdssq  12786  phiprmpw  12978  eulerthlemh  12987  odzdvds  13002  pc2dvds  13087  1arith  13124  issubg3  13972  eqgid  14006  resghm2b  14042  conjghm  14056  conjnmzb  14060  ablsubsub23  14106  issrgid  14259  isringid  14303  opprsubgg  14363  opprunitd  14390  crngunit  14391  unitpropdg  14428  issubrng  14480  opprsubrngg  14492  opprdrng  14593  lsslss  14690  lsspropdg  14740  rspsn  14843  znidom  14964  psrbagconf1o  14987  cnrest2  15260  cnptoprest  15263  cnptoprest2  15264  lmss  15270  lmff  15273  txlm  15303  ismet2  15378  blres  15458  xmetec  15461  bdbl  15527  metrest  15530  cnbl0  15558  cnblcld  15559  reopnap  15570  bl2ioo  15574  limcdifap  15686  efle  15800  reapef  15802  logleb  15899  logrpap0b  15900  cxplt  15941  cxple  15942  rpcxple2  15943  rpcxplt2  15944  cxplt3  15945  cxple3  15946  apcxp2  15964  logbleb  15986  logblt  15987  lgsdilem  16060  lgsne0  16071  lgsquadlem1  16110  lgsquadlem2  16111  m1lgs  16118  2lgslem1a  16121  2lgs  16137  ausgrusgrben  16323  uspgr2wlkeq  16520  isclwwlknx  16571  eupth2lem3lem6fi  16626  iooref1o  16988