Theorem 3imtr4d 286

Description: More general version of 3imtr4i 284. Useful for converting conditional definitions in a formula. (Contributed by NM, 26-Oct-1995.)

Hypotheses

Ref	Expression
3imtr4d.1	⊢ (𝜑 → (𝜓 → 𝜒))
3imtr4d.2	⊢ (𝜑 → (𝜃 ↔ 𝜓))
3imtr4d.3	⊢ (𝜑 → (𝜏 ↔ 𝜒))

Assertion

Ref	Expression
3imtr4d	⊢ (𝜑 → (𝜃 → 𝜏))

Proof of Theorem 3imtr4d

Step	Hyp	Ref	Expression
1		3imtr4d.2	. 2 ⊢ (𝜑 → (𝜃 ↔ 𝜓))
2		3imtr4d.1	. . 3 ⊢ (𝜑 → (𝜓 → 𝜒))
3		3imtr4d.3	. . 3 ⊢ (𝜑 → (𝜏 ↔ 𝜒))
4	2, 3	sylibrd 251	. 2 ⊢ (𝜑 → (𝜓 → 𝜏))
5	1, 4	sylbid 232	1 ⊢ (𝜑 → (𝜃 → 𝜏))

Syntax hints:   → wi 4   ↔ wb 198

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 199

This theorem is referenced by:  rmosn  4485  unielrel  5914  predpo  5951  fvrnressn  6694  fconst5  6743  soisores  6849  caofrss  7207  caoftrn  7209  f1o2ndf1  7566  oaord  7911  omord2  7931  omcan  7933  oeord  7952  oecan  7953  nnaord  7983  nnmord  7996  omsmo  8018  pmss12g  8167  cantnf  8887  pm54.43  9159  ttukeylem2  9667  axlttrn  10449  axltadd  10450  axmulgt0  10451  axsup  10452  ltadd2  10480  ltord1  10901  recex  11007  prodge0OLD  11224  ltmul1  11227  lt2msq  11262  nnge1  11404  zltp1le  11779  uzss  12013  eluzp1m1  12016  prodge0rd  12246  ixxssixx  12501  zesq  13306  swrdccatin12lem3  13860  swrdccat3blem  13871  relexpsucnnr  14172  climrlim2  14686  rlimres  14697  climshftlem  14713  lo1add  14765  lo1mul  14766  rlimsqzlem  14787  lo1le  14790  isercolllem2  14804  isercoll  14806  climsup  14808  cvgcmp  14952  climcndslem1  14985  dvds1lem  15400  sumodd  15518  algcvg  15695  eucalgcvga  15705  rpexp12i  15838  crth  15887  pc2dvds  15987  pcmpt  16000  prmpwdvds  16012  1arith  16035  vdwlem2  16090  vdwlem6  16094  vdwlem8  16096  ercpbl  16595  initoid  17040  termoid  17041  ipopos  17546  subginv  17985  symggrp  18203  f1otrspeq  18250  lsmless1x  18443  lsmless2x  18444  dprdss  18815  dvdsunit  19050  irredrmul  19094  isdrngd  19164  lspextmo  19451  evlseu  19912  domnchr  20276  zntoslem  20300  mat2pmatf1  20941  tgss  21180  neips  21325  opnnei  21332  lpss3  21356  ssrest  21388  t1t0  21560  kgen2ss  21767  isfild  22070  fgss  22085  fgss2  22086  cnpflf2  22212  fclsss1  22234  fclsss2  22235  tgpt0  22330  tsmsxp  22366  prdsxmslem2  22742  ngptgp  22848  nghmcn  22957  qdensere  22981  evth  23166  nmhmcn  23327  tcphcph  23443  caussi  23503  equivcfil  23505  rrxmvallem  23610  ivthlem2  23656  ovollb2lem  23692  ovolunlem1  23701  volun  23749  ioombl1lem4  23765  volsup2  23809  volcn  23810  ismbf3d  23858  itg2mulclem  23950  cpnord  24135  lhop1  24214  aaliou3lem2  24535  ulmclm  24578  ulmss  24588  abelth  24632  cosord  24716  efif1olem4  24729  argimgt0  24795  logdivlt  24804  cxploglim  25156  dvdssqf  25316  mumullem1  25357  mumullem2  25358  bposlem6  25466  lgsdchr  25532  gausslemma2dlem1a  25542  m1lgs  25565  chtppilim  25616  ax5seg  26287  axpasch  26290  axlowdimlem16  26306  axeuclid  26312  axcontlem4  26316  usgr1v0e  26673  nb3gr2nb  26732  cplgr1v  26778  finsumvtxdg2size  26898  usgr2pthlem  27115  clwwlknwwlksn  27427  erclwwlknsym  27468  erclwwlkntr  27469  frgr3vlem1  27681  3vfriswmgrlem  27685  numclwwlk5  27820  minvecolem5  28309  ocsh  28714  shless  28790  leopadd  29563  leopmuli  29564  leopmul2i  29566  leoptr  29568  spansncv2  29724  mdsl0  29741  ssdmd1  29744  cvdmd  29768  cdj3i  29872  uzssico  30110  eqgvscpbl  30408  qusvscpbl  30409  cmpcref  30515  cvmliftmolem1  31862  mrsubff1  32010  msubff1  32052  lediv2aALT  32168  sletr  32472  cgr3tr4  32748  colinearxfr  32771  lineext  32772  brsegle  32804  seglecgr12im  32806  segletr  32810  colinbtwnle  32814  outsideoftr  32825  lineelsb2  32844  ivthALT  32918  tailfb  32960  poimirlem29  34048  itg2addnclem  34070  itg2addnclem3  34072  itg2addnc  34073  incsequz  34152  mettrifi  34161  ismtycnv  34209  bfplem1  34229  ghomco  34298  rngoisocnv  34388  keridl  34439  dmncan1  34483  ax12indalem  35083  ax12inda2ALT  35084  omllaw4  35384  cmtcomlemN  35386  cvlexch2  35467  cvlatexch2  35475  cvrexch  35558  atexchltN  35579  3atlem5  35625  lplnribN  35689  linepsubN  35890  paddss1  35955  paddss2  35956  pmapjoin  35990  pmapjat1  35991  cdleme36a  36598  dib2dim  37381  dih2dimbALTN  37383  djhcvat42  37553  dihjatcclem4  37559  dihjat1lem  37566  lcfrlem6  37685  hlhillcs  38096  oexpreposd  38141  pell1234qrmulcl  38361  pell14qrss1234  38362  pell14qrmulcl  38369  pell14qrreccl  38370  pell1qrss14  38374  monotoddzzfi  38448  oddcomabszz  38450  climinf  40728  2ffzoeq  42352  iccpartgt  42377  upwlkwlk  42744  uspgrsprf1  42752  rrx2xpref1o  43436  itschlc0yqe  43478