Theorem 3imtr4d 297

Description: More general version of 3imtr4i 295. 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 262	. 2 ⊢ (𝜑 → (𝜓 → 𝜏))
5	1, 4	sylbid 243	1 ⊢ (𝜑 → (𝜃 → 𝜏))

Syntax hints:   → wi 4   ↔ wb 209

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 210

This theorem is referenced by:  rmosn  4615  unielrel  6093  predpo  6134  fvrnressn  6900  fconst5  6945  soisores  7059  caofrss  7422  caoftrn  7424  f1o2ndf1  7801  oaord  8156  omord2  8176  omcan  8178  oeord  8197  oecan  8198  nnaord  8228  nnmord  8241  omsmo  8264  pmss12g  8416  cantnf  9140  pm54.43  9414  ttukeylem2  9921  axlttrn  10702  axltadd  10703  axmulgt0  10704  axsup  10705  ltadd2  10733  ltord1  11155  recex  11261  ltmul1  11479  lt2msq  11514  nnge1  11653  zltp1le  12020  uzss  12253  eluzp1m1  12256  prodge0rd  12484  ixxssixx  12740  zesq  13583  pfxccatin12lem3  14085  swrdccat3blem  14092  relexpsucnnr  14376  climrlim2  14896  rlimres  14907  climshftlem  14923  lo1add  14975  lo1mul  14976  rlimsqzlem  14997  lo1le  15000  isercolllem2  15014  isercoll  15016  climsup  15018  cvgcmp  15163  climcndslem1  15196  dvds1lem  15613  sumodd  15729  algcvg  15910  eucalgcvga  15920  rpexp12i  16056  crth  16105  pc2dvds  16205  pcmpt  16218  prmpwdvds  16230  1arith  16253  vdwlem2  16308  vdwlem6  16312  vdwlem8  16314  ercpbl  16814  initoid  17257  termoid  17258  ipopos  17762  insubm  17975  subginv  18278  symggrp  18520  f1otrspeq  18567  lsmless1x  18761  lsmless2x  18762  dprdss  19144  dvdsunit  19409  irredrmul  19453  isdrngd  19520  lspextmo  19821  domnchr  20224  zntoslem  20248  evlseu  20755  mat2pmatf1  21334  tgss  21573  neips  21718  opnnei  21725  lpss3  21749  ssrest  21781  t1t0  21953  kgen2ss  22160  isfild  22463  fgss  22478  fgss2  22479  cnpflf2  22605  fclsss1  22627  fclsss2  22628  tgpt0  22724  tsmsxp  22760  prdsxmslem2  23136  ngptgp  23242  nghmcn  23351  qdensere  23375  evth  23564  nmhmcn  23725  tcphcph  23841  caussi  23901  equivcfil  23903  rrxmvallem  24008  ivthlem2  24056  ovollb2lem  24092  ovolunlem1  24101  volun  24149  ioombl1lem4  24165  volsup2  24209  volcn  24210  ismbf3d  24258  itg2mulclem  24350  cpnord  24538  lhop1  24617  aaliou3lem2  24939  ulmclm  24982  ulmss  24992  abelth  25036  cosord  25123  efif1olem4  25137  argimgt0  25203  logdivlt  25212  cxploglim  25563  dvdssqf  25723  mumullem1  25764  mumullem2  25765  bposlem6  25873  lgsdchr  25939  gausslemma2dlem1a  25949  m1lgs  25972  chtppilim  26059  ax5seg  26732  axpasch  26735  axlowdimlem16  26751  axeuclid  26757  axcontlem4  26761  usgr1v0e  27116  nb3gr2nb  27174  cplgr1v  27220  finsumvtxdg2size  27340  usgr2pthlem  27552  clwwlknwwlksn  27823  erclwwlknsym  27855  erclwwlkntr  27856  frgr3vlem1  28058  3vfriswmgrlem  28062  numclwwlk5  28173  minvecolem5  28664  ocsh  29066  shless  29142  leopadd  29915  leopmuli  29916  leopmul2i  29918  leoptr  29920  spansncv2  30076  mdsl0  30093  ssdmd1  30096  cvdmd  30120  cdj3i  30224  uzssico  30533  eqgvscpbl  30970  qusvscpbl  30971  cmpcref  31203  acycgrsubgr  32518  cvmliftmolem1  32641  satffunlem2lem2  32766  mrsubff1  32874  msubff1  32916  lediv2aALT  33033  sletr  33350  cgr3tr4  33626  colinearxfr  33649  lineext  33650  brsegle  33682  seglecgr12im  33684  segletr  33688  colinbtwnle  33692  outsideoftr  33703  lineelsb2  33722  ivthALT  33796  tailfb  33838  poimirlem29  35086  itg2addnclem  35108  itg2addnclem3  35110  itg2addnc  35111  incsequz  35186  mettrifi  35195  ismtycnv  35240  bfplem1  35260  ghomco  35329  rngoisocnv  35419  keridl  35470  dmncan1  35514  ax12indalem  36241  ax12inda2ALT  36242  omllaw4  36542  cmtcomlemN  36544  cvlexch2  36625  cvlatexch2  36633  cvrexch  36716  atexchltN  36737  3atlem5  36783  lplnribN  36847  linepsubN  37048  paddss1  37113  paddss2  37114  pmapjoin  37148  pmapjat1  37149  cdleme36a  37756  dib2dim  38539  dih2dimbALTN  38541  djhcvat42  38711  dihjatcclem4  38717  dihjat1lem  38724  lcfrlem6  38843  hlhillcs  39254  oexpreposd  39487  mulgt0b2d  39585  pell1234qrmulcl  39796  pell14qrss1234  39797  pell14qrmulcl  39804  pell14qrreccl  39805  pell1qrss14  39809  monotoddzzfi  39883  oddcomabszz  39885  climinf  42248  2ffzoeq  43885  iccpartgt  43944  upwlkwlk  44367  uspgrsprf1  44375  rrx2xpref1o  45132  itschlc0yqe  45174