Theorem 3imtr4d 295

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

Syntax hints:   → wi 4   ↔ wb 207

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 208

This theorem is referenced by:  rmosn  4651  unielrel  6225  predtrss  6273  fvrnressn  7104  fconst5  7150  soisores  7271  caofrss  7659  caoftrn  7661  f1o2ndf1  8061  oaord  8472  omord2  8492  omcan  8494  oeord  8514  oecan  8515  nnaord  8545  nnmord  8558  omsmo  8584  pmss12g  8807  cantnf  9605  pm54.43  9916  ttukeylem2  10423  axlttrn  11209  axltadd  11210  axmulgt0  11211  axsup  11212  ltadd2  11241  ltord1  11667  recex  11773  ltmul1  11996  lt2msq  12032  nnge1  12196  zltp1le  12568  uzss  12802  eluzp1m1  12805  prodge0rd  13042  ixxssixx  13303  zesq  14179  pfxccatin12lem3  14685  swrdccat3blem  14692  relexpsucnnr  14978  climrlim2  15500  rlimres  15511  climshftlem  15527  lo1add  15580  lo1mul  15581  rlimsqzlem  15602  lo1le  15605  isercolllem2  15619  isercoll  15621  climsup  15623  cvgcmp  15770  climcndslem1  15805  dvds1lem  16227  sumodd  16348  rprpwr  16519  algcvg  16536  eucalgcvga  16546  rpexp12i  16685  crth  16739  pc2dvds  16841  pcmpt  16854  prmpwdvds  16866  1arith  16889  vdwlem2  16944  vdwlem6  16948  vdwlem8  16950  ercpbl  17504  initoid  17959  termoid  17960  ipopos  18493  insubm  18777  subginv  19100  symggrp  19366  f1otrspeq  19413  lsmless1x  19610  lsmless2x  19611  dprdss  19997  rngpropd  20146  dvdsunit  20350  irredrmul  20398  isdrngd  20737  isdrngdOLD  20739  lspextmo  21046  rngqiprngimf1lem  21287  domnchr  21507  zntoslem  21531  evlseu  22059  mat2pmatf1  22712  tgss  22951  neips  23096  opnnei  23103  lpss3  23127  ssrest  23159  t1t0  23331  kgen2ss  23538  isfild  23841  fgss  23856  fgss2  23857  cnpflf2  23983  fclsss1  24005  fclsss2  24006  tgpt0  24102  tsmsxp  24138  prdsxmslem2  24512  ngptgp  24619  nghmcn  24728  qdensere  24752  evth  24944  nmhmcn  25105  tcphcph  25222  caussi  25282  equivcfil  25284  rrxmvallem  25389  ivthlem2  25437  ovollb2lem  25473  ovolunlem1  25482  volun  25530  ioombl1lem4  25546  volsup2  25590  volcn  25591  ismbf3d  25639  itg2mulclem  25731  cpnord  25920  lhop1  25999  aaliou3lem2  26327  ulmclm  26370  ulmss  26380  abelth  26424  cosord  26513  efif1olem4  26527  argimgt0  26594  logdivlt  26603  cxploglim  26959  dvdssqf  27119  mumullem1  27160  mumullem2  27161  bposlem6  27270  lgsdchr  27336  gausslemma2dlem1a  27346  m1lgs  27369  chtppilim  27456  lestr  27744  lestric  27750  madebdayim  27898  madebdaylemold  27908  ltslpss  27918  om2noseqf1o  28311  zsoring  28419  bdaypw2n0bndlem  28473  bdayfin  28497  ax5seg  29025  axpasch  29028  axlowdimlem16  29044  axeuclid  29050  axcontlem4  29054  usgr1v0e  29413  nb3gr2nb  29471  cplgr1v  29517  finsumvtxdg2size  29637  usgr2pthlem  29849  clwwlknwwlksn  30126  erclwwlknsym  30158  erclwwlkntr  30159  frgr3vlem1  30361  3vfriswmgrlem  30365  numclwwlk5  30476  minvecolem5  30970  ocsh  31372  shless  31448  leopadd  32221  leopmuli  32222  leopmul2i  32224  leoptr  32226  spansncv2  32382  mdsl0  32399  ssdmd1  32402  cvdmd  32426  cdj3i  32530  uzssico  32876  expgt0b  32909  eqgvscpbl  33433  qusvscpbl  33434  cmpcref  34034  acycgrsubgr  35386  cvmliftmolem1  35509  satffunlem2lem2  35634  mrsubff1  35742  msubff1  35784  lediv2aALT  35905  cgr3tr4  36280  colinearxfr  36303  lineext  36304  brsegle  36336  seglecgr12im  36338  segletr  36342  colinbtwnle  36346  outsideoftr  36357  lineelsb2  36376  ivthALT  36563  tailfb  36605  poimirlem29  38016  itg2addnclem  38038  itg2addnclem3  38040  itg2addnc  38041  incsequz  38115  mettrifi  38124  ismtycnv  38169  bfplem1  38189  ghomco  38258  rngoisocnv  38348  keridl  38399  dmncan1  38443  ax12indalem  39437  ax12inda2ALT  39438  omllaw4  39738  cmtcomlemN  39740  cvlexch2  39821  cvlatexch2  39829  cvrexch  39912  atexchltN  39933  3atlem5  39979  lplnribN  40043  linepsubN  40244  paddss1  40309  paddss2  40310  pmapjoin  40344  pmapjat1  40345  cdleme36a  40952  dib2dim  41735  dih2dimbALTN  41737  djhcvat42  41907  dihjatcclem4  41913  dihjat1lem  41920  lcfrlem6  42039  hlhillcs  42450  oexpreposd  42799  mulgt0b1d  42962  mullt0b1d  42973  pell1234qrmulcl  43300  pell14qrss1234  43301  pell14qrmulcl  43308  pell14qrreccl  43309  pell1qrss14  43313  monotoddzzfi  43387  oddcomabszz  43389  omabs2  43777  omcl3g  43779  tfsconcat0b  43791  naddwordnexlem4  43846  climinf  46051  2ffzoeq  47791  iccpartgt  47902  pgnbgreunbgrlem1  48604  pgnbgreunbgrlem4  48610  upwlkwlk  48630  uspgrsprf1  48638  rrx2xpref1o  49209  itschlc0yqe  49251  resipos  49465