Theorem mpand 694

Description: A deduction based on modus ponens. (Contributed by NM, 12-Dec-2004.) (Proof shortened by Wolf Lammen, 7-Apr-2013.)

Hypotheses

Ref	Expression
mpand.1	⊢ (𝜑 → 𝜓)
mpand.2	⊢ (𝜑 → ((𝜓 ∧ 𝜒) → 𝜃))

Assertion

Ref	Expression
mpand	⊢ (𝜑 → (𝜒 → 𝜃))

Proof of Theorem mpand

Step	Hyp	Ref	Expression
1		mpand.1	. 2 ⊢ (𝜑 → 𝜓)
2		mpand.2	. . 3 ⊢ (𝜑 → ((𝜓 ∧ 𝜒) → 𝜃))
3	2	ancomsd 467	. 2 ⊢ (𝜑 → ((𝜒 ∧ 𝜓) → 𝜃))
4	1, 3	mpan2d 693	1 ⊢ (𝜑 → (𝜒 → 𝜃))

Syntax hints:   → wi 4   ∧ wa 397

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 206  df-an 398

This theorem is referenced by:  mpani  695  mp2and  698  ecase2dOLD  1030  disjss3  5148  sotri2  6131  fpropnf1  7266  ovig  7554  orduniorsuc  7818  omopth2  8584  onomeneq  9228  frfi  9288  ordunifi  9293  finsschain  9359  cantnfp1lem3  9675  cantnfp1  9676  p1le  12059  nnge1  12240  zltp1le  12612  gtndiv  12639  uzss  12845  eluzaddOLD  12857  uzm1  12860  addlelt  13088  xrre2  13149  xrre3  13150  xrmaxlt  13160  xrmaxle  13162  xrsupsslem  13286  xrub  13291  supxrunb1  13298  zltaddlt1le  13482  nn0p1elfzo  13675  elfzoext  13689  flflp1  13772  ceile  13814  modfzo0difsn  13908  seqf1olem1  14007  leexp2r  14139  expnlbnd2  14197  facavg  14261  wrdred1hash  14511  ccat2s1fvw  14588  caubnd2  15304  limsupbnd1  15426  limsupbnd2  15427  rlim2lt  15441  rlim3  15442  o1co  15530  mulcn2  15540  cn1lem  15542  rlimo1  15561  climsqz  15585  climsqz2  15586  rlimsqzlem  15595  lo1le  15598  rlimno1  15600  climsup  15616  caucvgrlem2  15621  iseraltlem2  15629  iseralt  15631  fsumabs  15747  cvgcmp  15762  cvgcmpce  15764  isumltss  15794  cvgrat  15829  ruclem9  16181  ruclem12  16184  bitsfzolem  16375  bitsfzo  16376  sadcaddlem  16398  gcdzeq  16494  algcvgblem  16514  algcvga  16516  lcmdvdsb  16550  lcmftp  16573  coprm  16648  eulerthlem2  16715  pclem  16771  infpn2  16846  prmreclem1  16849  prmreclem4  16852  ramtlecl  16933  prmgaplem7  16990  initoeu2  17966  lubval  18309  lublecllem  18313  glbval  18322  joinle  18339  latmlem1  18422  odmulg  19424  efginvrel2  19595  pgpfac1lem5  19949  chfacfscmul0  22360  chfacfpmmul0  22364  1stccnp  22966  qustgplem  23625  imasdsf1olem  23879  bldisj  23904  xbln0  23920  prdsbl  24000  metss2lem  24020  stdbdxmet  24024  ngptgp  24145  nghmcn  24262  icoopnst  24455  iocopnst  24456  cnllycmp  24472  iscau3  24795  cmetcaulem  24805  iscmet3lem1  24808  bcthlem4  24844  ovollb2lem  25005  ovolicc2lem3  25036  voliunlem3  25069  volcn  25123  itg10a  25228  itg1ge0a  25229  bddiblnc  25359  dvcnvrelem1  25534  dvfsumrlim  25548  itgsubst  25566  ulmcn  25911  ulmdvlem3  25914  mtest  25916  tanord  26047  emcllem6  26505  ftalem2  26578  chtub  26715  fsumvma2  26717  vmasum  26719  chpchtsum  26722  bcmono  26780  bclbnd  26783  bposlem1  26787  bposlem5  26791  bposlem6  26792  lgsne0  26838  gausslemma2dlem1a  26868  chtppilim  26978  dchrisumlem3  26994  pntrsumbnd2  27070  pntlemf  27108  pntlem3  27112  pntleml  27114  nosupno  27206  noinfno  27221  mulsproplem6  27577  mulsproplem7  27578  upgr2pthnlp  28989  crctcshwlkn0lem3  29066  crctcshwlkn0lem5  29068  eupth2lems  29491  grpoidinvlem3  29759  grpoideu  29762  vacn  29947  blocni  30058  ubthlem2  30124  chscllem2  30891  lnconi  31286  pjnmopi  31401  atomli  31635  sumdmdlem2  31672  cdj3lem2b  31690  xraddge02  31969  fedgmullem1  32714  dfon2lem5  34759  dfon2lem6  34760  cgrcoml  34968  btwnconn2  35074  fvineqsneq  36293  pibt2  36298  ltflcei  36476  poimirlem2  36490  poimirlem18  36506  poimirlem22  36510  poimirlem23  36511  poimirlem26  36514  poimirlem29  36517  poimirlem30  36518  poimirlem32  36520  heicant  36523  mblfinlem3  36527  mblfinlem4  36528  itg2addnclem  36539  itg2addnc  36542  ftc1anclem6  36566  ftc1anc  36569  mettrifi  36625  geomcau  36627  equivbnd  36658  heibor1lem  36677  bfplem1  36690  bfplem2  36691  rrncmslem  36700  divrngidl  36896  lecmtN  38126  cvrletrN  38143  llnnleat  38384  lplnnle2at  38412  lvolnle3at  38453  dalem21  38565  cdlemblem  38664  osumcllem11N  38837  pexmidlem8N  38848  lhpmcvr4N  38897  cdleme32b  39313  cdleme35fnpq  39320  cdleme48bw  39373  cdlemf1  39432  cdlemg2fv2  39471  cdlemg7fvbwN  39478  cdlemg27b  39567  tendoeq2  39645  dia2dimlem1  39935  dihord6apre  40127  dihord5apre  40133  dihglbcpreN  40171  dochnel2  40263  dihjat1lem  40299  dochexmidlem8  40338  mapdordlem2  40508  eqresfnbd  41054  3cubeslem1  41422  ordnexbtwnsuc  42017  naddcnfid2  42118  nadd2rabex  42136  iscard5  42287  frege124d  42512  mnringmulrcld  42987  climinf  44322  2ffzoeq  46036  iccpartlt  46092  lighneallem2  46274  bgoldbtbndlem3  46475  bgoldbtbndlem4  46476  tgoldbach  46485  fllog2  47254  dignn0ldlem  47288