Theorem 3imtr4d 294

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

Syntax hints:   → wi 4   ↔ wb 206

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 207

This theorem is referenced by:  rmosn  4676  unielrel  6232  predtrss  6280  fvrnressn  7106  fconst5  7152  soisores  7273  caofrss  7661  caoftrn  7663  f1o2ndf1  8064  oaord  8474  omord2  8494  omcan  8496  oeord  8516  oecan  8517  nnaord  8547  nnmord  8560  omsmo  8586  pmss12g  8807  cantnf  9602  pm54.43  9913  ttukeylem2  10420  axlttrn  11205  axltadd  11206  axmulgt0  11207  axsup  11208  ltadd2  11237  ltord1  11663  recex  11769  ltmul1  11991  lt2msq  12027  nnge1  12173  zltp1le  12541  uzss  12774  eluzp1m1  12777  prodge0rd  13014  ixxssixx  13275  zesq  14149  pfxccatin12lem3  14655  swrdccat3blem  14662  relexpsucnnr  14948  climrlim2  15470  rlimres  15481  climshftlem  15497  lo1add  15550  lo1mul  15551  rlimsqzlem  15572  lo1le  15575  isercolllem2  15589  isercoll  15591  climsup  15593  cvgcmp  15739  climcndslem1  15772  dvds1lem  16194  sumodd  16315  rprpwr  16486  algcvg  16503  eucalgcvga  16513  rpexp12i  16651  crth  16705  pc2dvds  16807  pcmpt  16820  prmpwdvds  16832  1arith  16855  vdwlem2  16910  vdwlem6  16914  vdwlem8  16916  ercpbl  17470  initoid  17925  termoid  17926  ipopos  18459  insubm  18743  subginv  19063  symggrp  19329  f1otrspeq  19376  lsmless1x  19573  lsmless2x  19574  dprdss  19960  rngpropd  20109  dvdsunit  20315  irredrmul  20363  isdrngd  20698  isdrngdOLD  20700  lspextmo  21008  rngqiprngimf1lem  21249  domnchr  21487  zntoslem  21511  evlseu  22038  mat2pmatf1  22673  tgss  22912  neips  23057  opnnei  23064  lpss3  23088  ssrest  23120  t1t0  23292  kgen2ss  23499  isfild  23802  fgss  23817  fgss2  23818  cnpflf2  23944  fclsss1  23966  fclsss2  23967  tgpt0  24063  tsmsxp  24099  prdsxmslem2  24473  ngptgp  24580  nghmcn  24689  qdensere  24713  evth  24914  nmhmcn  25076  tcphcph  25193  caussi  25253  equivcfil  25255  rrxmvallem  25360  ivthlem2  25409  ovollb2lem  25445  ovolunlem1  25454  volun  25502  ioombl1lem4  25518  volsup2  25562  volcn  25563  ismbf3d  25611  itg2mulclem  25703  cpnord  25893  lhop1  25975  aaliou3lem2  26307  ulmclm  26352  ulmss  26362  abelth  26407  cosord  26496  efif1olem4  26510  argimgt0  26577  logdivlt  26586  cxploglim  26944  dvdssqf  27104  mumullem1  27145  mumullem2  27146  bposlem6  27256  lgsdchr  27322  gausslemma2dlem1a  27332  m1lgs  27355  chtppilim  27442  lestr  27730  lestric  27736  madebdayim  27884  madebdaylemold  27894  ltslpss  27904  om2noseqf1o  28297  zsoring  28405  bdaypw2n0bndlem  28459  bdayfin  28483  ax5seg  29011  axpasch  29014  axlowdimlem16  29030  axeuclid  29036  axcontlem4  29040  usgr1v0e  29399  nb3gr2nb  29457  cplgr1v  29503  finsumvtxdg2size  29624  usgr2pthlem  29836  clwwlknwwlksn  30113  erclwwlknsym  30145  erclwwlkntr  30146  frgr3vlem1  30348  3vfriswmgrlem  30352  numclwwlk5  30463  minvecolem5  30956  ocsh  31358  shless  31434  leopadd  32207  leopmuli  32208  leopmul2i  32210  leoptr  32212  spansncv2  32368  mdsl0  32385  ssdmd1  32388  cvdmd  32412  cdj3i  32516  uzssico  32864  expgt0b  32897  eqgvscpbl  33431  qusvscpbl  33432  cmpcref  34007  acycgrsubgr  35352  cvmliftmolem1  35475  satffunlem2lem2  35600  mrsubff1  35708  msubff1  35750  lediv2aALT  35871  cgr3tr4  36246  colinearxfr  36269  lineext  36270  brsegle  36302  seglecgr12im  36304  segletr  36308  colinbtwnle  36312  outsideoftr  36323  lineelsb2  36342  ivthALT  36529  tailfb  36571  poimirlem29  37850  itg2addnclem  37872  itg2addnclem3  37874  itg2addnc  37875  incsequz  37949  mettrifi  37958  ismtycnv  38003  bfplem1  38023  ghomco  38092  rngoisocnv  38182  keridl  38233  dmncan1  38277  ax12indalem  39205  ax12inda2ALT  39206  omllaw4  39506  cmtcomlemN  39508  cvlexch2  39589  cvlatexch2  39597  cvrexch  39680  atexchltN  39701  3atlem5  39747  lplnribN  39811  linepsubN  40012  paddss1  40077  paddss2  40078  pmapjoin  40112  pmapjat1  40113  cdleme36a  40720  dib2dim  41503  dih2dimbALTN  41505  djhcvat42  41675  dihjatcclem4  41681  dihjat1lem  41688  lcfrlem6  41807  hlhillcs  42218  oexpreposd  42577  mulgt0b1d  42727  mullt0b1d  42738  pell1234qrmulcl  43097  pell14qrss1234  43098  pell14qrmulcl  43105  pell14qrreccl  43106  pell1qrss14  43110  monotoddzzfi  43184  oddcomabszz  43186  omabs2  43574  omcl3g  43576  tfsconcat0b  43588  naddwordnexlem4  43643  climinf  45852  2ffzoeq  47573  iccpartgt  47673  pgnbgreunbgrlem1  48359  pgnbgreunbgrlem4  48365  upwlkwlk  48385  uspgrsprf1  48393  rrx2xpref1o  48964  itschlc0yqe  49006  resipos  49220