Theorem mpand 707

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

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

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 401

This theorem is used by:  mpani  708  mp2and  711  disjss3  5107  sotri2  6128  fpropnf1  7265  ovig  7558  orduniorsuc  7824  resf1ext2b  7930  omopth2  8567  onomeneq  9196  frfi  9243  ordunifi  9248  finsschain  9314  cantnfp1lem3  9647  cantnfp1  9648  p1le  12066  nnge1  12270  zltp1le  12650  gtndiv  12679  uzss  12891  uzm1  12902  addlelt  13138  xrre2  13202  xrre3  13203  xrmaxlt  13213  xrmaxle  13215  xrsupsslem  13339  xrub  13344  supxrunb1  13351  zltaddlt1le  13538  nn0p1elfzo  13738  flflp1  13847  ceile  13889  modfzo0difsn  13986  seqf1olem1  14084  leexp2r  14217  expnlbnd2  14277  facavg  14344  wrdred1hash  14605  ccat2s1fvw  14683  caubnd2  15416  limsupbnd1  15540  limsupbnd2  15541  rlim2lt  15555  rlim3  15556  o1co  15644  mulcn2  15654  cn1lem  15656  rlimo1  15675  climsqz  15699  climsqz2  15700  rlimsqzlem  15707  lo1le  15710  rlimno1  15712  climsup  15728  caucvgrlem2  15733  iseraltlem2  15741  iseralt  15743  fsumabs  15860  cvgcmp  15875  cvgcmpce  15877  isumltss  15909  cvgrat  15944  ruclem9  16300  ruclem12  16303  bitsfzolem  16498  bitsfzo  16499  sadcaddlem  16521  gcdzeq  16616  algcvgblem  16641  algcvga  16643  lcmdvdsb  16677  lcmftp  16700  coprm  16776  eulerthlem2  16847  pclem  16904  infpn2  16979  prmreclem1  16982  prmreclem4  16985  ramtlecl  17066  prmgaplem7  17123  initoeu2  18079  lubval  18416  lublecllem  18420  glbval  18429  joinle  18446  latmlem1  18531  odmulg  19632  efginvrel2  19803  pgpfac1lem5  20157  chfacfscmul0  23026  chfacfpmmul0  23030  1stccnp  23630  qustgplem  24289  imasdsf1olem  24541  bldisj  24566  xbln0  24582  prdsbl  24659  metss2lem  24679  stdbdxmet  24683  ngptgp  24804  nghmcn  24913  icoopnst  25109  iocopnst  25110  cnllycmp  25126  iscau3  25448  cmetcaulem  25458  iscmet3lem1  25461  bcthlem4  25497  ovollb2lem  25658  ovolicc2lem3  25689  voliunlem3  25722  volcn  25776  itg10a  25880  itg1ge0a  25881  bddiblnc  26012  dvcnvrelem1  26187  dvfsumrlim  26201  itgsubst  26219  ulmcn  26573  ulmdvlem3  26576  mtest  26578  tanord  26714  emcllem6  27176  ftalem2  27249  chtub  27387  fsumvma2  27389  vmasum  27391  chpchtsum  27394  bcmono  27452  bclbnd  27455  bposlem1  27459  bposlem5  27463  bposlem6  27464  lgsne0  27510  gausslemma2dlem1a  27540  chtppilim  27650  dchrisumlem3  27666  pntrsumbnd2  27742  pntlemf  27780  pntlem3  27784  pntleml  27786  nosupno  27878  noinfno  27893  mulsproplem6  28325  mulsproplem7  28326  upgr2pthnlp  30092  crctcshwlkn0lem3  30172  crctcshwlkn0lem5  30174  eupth2lems  30600  grpoidinvlem3  30869  grpoideu  30872  vacn  31057  blocni  31168  ubthlem2  31234  chscllem2  32001  lnconi  32396  pjnmopi  32511  atomli  32745  sumdmdlem2  32782  cdj3lem2b  32800  xraddge02  33113  fedgmullem1  34028  dfon2lem5  36285  dfon2lem6  36286  cgrcoml  36496  btwnconn2  36602  fvineqsneq  38086  pibt2  38091  ltflcei  38287  poimirlem2  38301  poimirlem18  38317  poimirlem22  38321  poimirlem23  38322  poimirlem26  38325  poimirlem29  38328  poimirlem30  38329  poimirlem32  38331  heicant  38334  mblfinlem3  38338  mblfinlem4  38339  itg2addnclem  38350  itg2addnc  38353  ftc1anclem6  38377  ftc1anc  38380  mettrifi  38436  geomcau  38438  equivbnd  38469  heibor1lem  38488  bfplem1  38501  bfplem2  38502  rrncmslem  38511  divrngidl  38707  preuniqval  39173  lecmtN  40058  cvrletrN  40075  llnnleat  40315  lplnnle2at  40343  lvolnle3at  40384  dalem21  40496  cdlemblem  40595  osumcllem11N  40768  pexmidlem8N  40779  lhpmcvr4N  40828  cdleme32b  41244  cdleme35fnpq  41251  cdleme48bw  41304  cdlemf1  41363  cdlemg2fv2  41402  cdlemg7fvbwN  41409  cdlemg27b  41498  tendoeq2  41576  dia2dimlem1  41866  dihord6apre  42058  dihord5apre  42064  dihglbcpreN  42102  dochnel2  42194  dihjat1lem  42230  dochexmidlem8  42269  mapdordlem2  42439  eqresfnbd  43031  3cubeslem1  43443  ordnexbtwnsuc  44022  naddcnfid2  44123  nadd2rabex  44141  iscard5  44290  frege124d  44515  mnringmulrcld  44980  climinf  46350  2ffzoeq  48093  iccpartlt  48201  lighneallem2  48386  bgoldbtbndlem3  48600  bgoldbtbndlem4  48601  tgoldbach  48610  fllog2  49376  dignn0ldlem  49410