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

Syntax hints:   → wi 4   ∧ wa 383

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 196  df-an 385

This theorem is referenced by:  mpani  708  mp2and  711  ecase2d  978  disjss3  4582  sotri2  5444  ovig  6680  orduniorsuc  6922  omopth2  7551  frfi  8090  ordunifi  8095  finsschain  8156  cantnfp1lem3  8460  cantnfp1  8461  p1le  10745  nnge1  10923  zltp1le  11304  gtndiv  11330  uzss  11584  eluzadd  11592  uzm1  11594  addlelt  11818  xrre2  11875  xrre3  11876  xrmaxlt  11886  xrmaxle  11888  xrsupsslem  12009  xrub  12014  supxrunb1  12021  zltaddlt1le  12195  nn0p1elfzo  12378  elfzoext  12392  flflp1  12470  ceile  12510  modfzo0difsn  12604  seqf1olem1  12702  leexp2r  12780  expnlbnd2  12857  facavg  12950  ccat2s1fvw  13267  caubnd2  13945  limsupbnd1  14061  limsupbnd2  14062  rlim2lt  14076  rlim3  14077  o1co  14165  mulcn2  14174  cn1lem  14176  rlimo1  14195  climsqz  14219  climsqz2  14220  rlimsqzlem  14227  lo1le  14230  rlimno1  14232  climsup  14248  caucvgrlem2  14253  iseraltlem2  14261  iseralt  14263  fsumabs  14374  cvgcmp  14389  cvgcmpce  14391  isumltss  14419  cvgrat  14454  ruclem9  14806  ruclem12  14809  bitsfzolem  14994  bitsfzo  14995  sadcaddlem  15017  gcdzeq  15109  algcvgblem  15128  algcvga  15130  lcmdvdsb  15164  lcmftp  15187  coprmdvdsOLD  15205  coprm  15261  eulerthlem2  15325  pclem  15381  infpn2  15455  prmreclem1  15458  prmreclem4  15461  ramtlecl  15542  prmgaplem7  15599  initoeu2  16489  lubval  16807  lublecllem  16811  glbval  16820  joinle  16837  latmlem1  16904  odmulg  17796  efginvrel2  17963  pgpfac1lem5  18301  chfacfscmul0  20482  chfacfpmmul0  20486  1stccnp  21075  qustgplem  21734  imasdsf1olem  21988  bldisj  22013  xbln0  22029  prdsbl  22106  metss2lem  22126  stdbdxmet  22130  ngptgp  22250  nghmcn  22359  icoopnst  22546  iocopnst  22547  cnllycmp  22563  iscau3  22884  cmetcaulem  22894  iscmet3lem1  22897  bcthlem4  22932  ovollb2lem  23063  ovolicc2lem3  23094  voliunlem3  23127  volcn  23180  itg10a  23283  itg1ge0a  23284  dvcnvrelem1  23584  dvfsumrlim  23598  itgsubst  23616  ulmcn  23957  ulmdvlem3  23960  mtest  23962  tanord  24088  emcllem6  24527  ftalem2  24600  chtub  24737  fsumvma2  24739  vmasum  24741  chpchtsum  24744  bcmono  24802  bclbnd  24805  bposlem1  24809  bposlem5  24813  bposlem6  24814  lgsne0  24860  gausslemma2dlem1a  24890  chtppilim  24964  dchrisumlem3  24980  pntrsumbnd2  25056  pntlemf  25094  pntlem3  25098  pntleml  25100  redwlklem  26135  eupath2  26507  grpoidinvlem3  26744  grpoideu  26747  vacn  26933  blocni  27044  ubthlem2  27111  chscllem2  27881  lnconi  28276  pjnmopi  28391  atomli  28625  sumdmdlem2  28662  cdj3lem2b  28680  xraddge02  28911  dfon2lem5  30936  dfon2lem6  30937  cgrcoml  31273  btwnconn2  31379  ltflcei  32567  poimirlem2  32581  poimirlem18  32597  poimirlem22  32601  poimirlem23  32602  poimirlem26  32605  poimirlem29  32608  poimirlem30  32609  poimirlem32  32611  heicant  32614  mblfinlem3  32618  mblfinlem4  32619  itg2addnclem  32631  itg2addnc  32634  bddiblnc  32650  ftc1anclem6  32660  ftc1anc  32663  mettrifi  32723  geomcau  32725  equivbnd  32759  heibor1lem  32778  bfplem1  32791  bfplem2  32792  rrncmslem  32801  divrngidl  32997  lecmtN  33561  cvrletrN  33578  llnnleat  33817  lplnnle2at  33845  lvolnle3at  33886  dalem21  33998  cdlemblem  34097  osumcllem11N  34270  pexmidlem8N  34281  lhpmcvr4N  34330  cdleme32b  34748  cdleme35fnpq  34755  cdleme48bw  34808  cdlemf1  34867  cdlemg2fv2  34906  cdlemg7fvbwN  34913  cdlemg27b  35002  tendoeq2  35080  dia2dimlem1  35371  dihord6apre  35563  dihord5apre  35569  dihglbcpreN  35607  dochnel2  35699  dihjat1lem  35735  dochexmidlem8  35774  mapdordlem2  35944  frege124d  37072  climinf  38673  iccpartlt  39962  lighneallem2  40061  bgoldbtbndlem3  40223  bgoldbtbndlem4  40224  tgoldbach  40232  tgoldbachOLD  40239  wrdred1hash  40241  fpropnf1  40337  2ffzoeq  40361  upgr2pthnlp  40938  crctcsh1wlkn0lem3  41015  crctcsh1wlkn0lem5  41017  eupth2lems  41406  fllog2  42160  dignn0ldlem  42194