Theorem mpand 708

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 471	. 2 ⊢ (𝜑 → ((𝜒 ∧ 𝜓) → 𝜃))
4	1, 3	mpan2d 707	1 ⊢ (𝜑 → (𝜒 → 𝜃))

This proof depends on syntax axioms:   → wi 4   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  mpani  709  mp2and  712  disjss3  5101  sotri2  6122  fpropnf1  7271  ovig  7566  orduniorsuc  7841  resf1ext2b  7947  omopth2  8592  onomeneq  9229  frfi  9276  ordunifi  9281  finsschain  9348  cantnfp1lem3  9681  cantnfp1  9682  p1le  12162  nnge1  12366  zltp1le  12746  gtndiv  12776  uzss  12988  uzm1  12999  addlelt  13236  xrre2  13300  xrre3  13301  xrmaxlt  13311  xrmaxle  13313  xrsupsslem  13437  xrub  13442  supxrunb1  13449  zltaddlt1le  13636  nn0p1elfzo  13837  flflp1  13947  ceile  13989  modfzo0difsn  14086  seqf1olem1  14184  leexp2r  14317  expnlbnd2  14378  facavg  14445  wrdred1hash  14706  ccat2s1fvw  14786  caubnd2  15525  limsupbnd1  15649  limsupbnd2  15650  rlim2lt  15664  rlim3  15665  o1co  15753  mulcn2  15763  cn1lem  15765  rlimo1  15784  climsqz  15808  climsqz2  15809  rlimsqzlem  15816  lo1le  15819  rlimno1  15821  climsup  15837  caucvgrlem2  15842  iseraltlem2  15850  iseralt  15852  fsumabs  15968  cvgcmp  15983  cvgcmpce  15985  isumltss  16017  cvgrat  16052  ruclem9  16406  ruclem12  16409  bitsfzolem  16604  bitsfzo  16605  sadcaddlem  16627  gcdzeq  16725  algcvgblem  16752  algcvga  16754  lcmdvdsb  16788  lcmftp  16811  coprm  16887  eulerthlem2  16959  pclem  17016  infpn2  17091  prmreclem1  17094  prmreclem4  17097  ramtlecl  17178  prmgaplem7  17235  initoeu2  18191  lubval  18528  lublecllem  18532  glbval  18541  joinle  18558  latmlem1  18643  odmulg  19770  efginvrel2  19941  pgpfac1lem5  20295  chfacfscmul0  23176  chfacfpmmul0  23180  1stccnp  23781  qustgplem  24440  imasdsf1olem  24692  bldisj  24717  xbln0  24733  prdsbl  24810  metss2lem  24830  stdbdxmet  24834  ngptgp  24955  nghmcn  25064  icoopnst  25260  iocopnst  25261  cnllycmp  25277  iscau3  25599  cmetcaulem  25609  iscmet3lem1  25612  bcthlem4  25648  ovollb2lem  25809  ovolicc2lem3  25840  voliunlem3  25873  volcn  25927  itg10a  26031  itg1ge0a  26032  bddiblnc  26162  dvcnvrelem1  26337  dvfsumrlim  26351  itgsubst  26369  ulmcn  26726  ulmdvlem3  26729  mtest  26731  tanord  26866  emcllem6  27328  ftalem2  27401  chtub  27539  fsumvma2  27541  vmasum  27543  chpchtsum  27546  bcmono  27604  bclbnd  27607  bposlem1  27611  bposlem5  27615  bposlem6  27616  lgsne0  27662  gausslemma2dlem1a  27692  chtppilim  27802  dchrisumlem3  27818  pntrsumbnd2  27894  pntlemf  27932  pntlem3  27936  pntleml  27938  nosupno  28060  noinfno  28075  mulsproplem6  28507  mulsproplem7  28508  upgr2pthnlp  30318  crctcshwlkn0lem3  30401  crctcshwlkn0lem5  30403  eupth2lems  30839  grpoidinvlem3  31108  grpoideu  31111  vacn  31296  blocni  31407  ubthlem2  31473  chscllem2  32240  lnconi  32635  pjnmopi  32750  atomli  32984  sumdmdlem2  33021  cdj3lem2b  33039  xraddge02  33391  fedgmullem1  34303  dfon2lem5  36591  dfon2lem6  36592  cgrcoml  36803  btwnconn2  36909  fvineqsneq  38378  pibt2  38383  ltflcei  38574  poimirlem2  38583  poimirlem18  38599  poimirlem22  38603  poimirlem23  38604  poimirlem26  38607  poimirlem29  38610  poimirlem30  38611  poimirlem32  38613  heicant  38616  mblfinlem3  38620  mblfinlem4  38621  itg2addnclem  38632  itg2addnc  38635  ftc1anclem6  38659  ftc1anc  38662  mettrifi  38734  geomcau  38736  equivbnd  38767  heibor1lem  38786  bfplem1  38799  bfplem2  38800  rrncmslem  38809  divrngidl  39005  preuniqval  39471  lecmtN  40356  cvrletrN  40373  llnnleat  40613  lplnnle2at  40641  lvolnle3at  40682  dalem21  40794  cdlemblem  40893  osumcllem11N  41066  pexmidlem8N  41077  lhpmcvr4N  41126  cdleme32b  41542  cdleme35fnpq  41549  cdleme48bw  41602  cdlemf1  41661  cdlemg2fv2  41700  cdlemg7fvbwN  41707  cdlemg27b  41796  tendoeq2  41874  dia2dimlem1  42164  dihord6apre  42356  dihord5apre  42362  dihglbcpreN  42400  dochnel2  42492  dihjat1lem  42528  dochexmidlem8  42567  mapdordlem2  42737  eqresfnbd  43329  3cubeslem1  43737  ordnexbtwnsuc  44312  naddcnfid2  44413  nadd2rabex  44431  iscard5  44580  frege124d  44804  mnringmulrcld  45269  climinf  46661  2ffzoeq  48441  iccpartlt  48549  lighneallem2  48734  bgoldbtbndlem3  48948  bgoldbtbndlem4  48949  tgoldbach  48958  fllog2  49723  dignn0ldlem  49757