Theorem mpand 693

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 692	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  694  mp2and  697  ecase2dOLD  1029  disjss3  5080  sotri2  6049  fpropnf1  7172  ovig  7451  orduniorsuc  7709  omopth2  8446  onomeneq  9049  frfi  9103  ordunifi  9108  finsschain  9170  cantnfp1lem3  9482  cantnfp1  9483  p1le  11866  nnge1  12047  zltp1le  12416  gtndiv  12443  uzss  12651  eluzadd  12659  uzm1  12662  addlelt  12890  xrre2  12950  xrre3  12951  xrmaxlt  12961  xrmaxle  12963  xrsupsslem  13087  xrub  13092  supxrunb1  13099  zltaddlt1le  13283  nn0p1elfzo  13476  elfzoext  13490  flflp1  13573  ceile  13615  modfzo0difsn  13709  seqf1olem1  13808  leexp2r  13938  expnlbnd2  13995  facavg  14061  wrdred1hash  14309  ccat2s1fvw  14394  ccat2s1fvwOLD  14395  caubnd2  15114  limsupbnd1  15236  limsupbnd2  15237  rlim2lt  15251  rlim3  15252  o1co  15340  mulcn2  15350  cn1lem  15352  rlimo1  15371  climsqz  15395  climsqz2  15396  rlimsqzlem  15405  lo1le  15408  rlimno1  15410  climsup  15426  caucvgrlem2  15431  iseraltlem2  15439  iseralt  15441  fsumabs  15558  cvgcmp  15573  cvgcmpce  15575  isumltss  15605  cvgrat  15640  ruclem9  15992  ruclem12  15995  bitsfzolem  16186  bitsfzo  16187  sadcaddlem  16209  gcdzeq  16307  algcvgblem  16327  algcvga  16329  lcmdvdsb  16363  lcmftp  16386  coprm  16461  eulerthlem2  16528  pclem  16584  infpn2  16659  prmreclem1  16662  prmreclem4  16665  ramtlecl  16746  prmgaplem7  16803  initoeu2  17776  lubval  18119  lublecllem  18123  glbval  18132  joinle  18149  latmlem1  18232  odmulg  19208  efginvrel2  19378  pgpfac1lem5  19727  chfacfscmul0  22052  chfacfpmmul0  22056  1stccnp  22658  qustgplem  23317  imasdsf1olem  23571  bldisj  23596  xbln0  23612  prdsbl  23692  metss2lem  23712  stdbdxmet  23716  ngptgp  23837  nghmcn  23954  icoopnst  24147  iocopnst  24148  cnllycmp  24164  iscau3  24487  cmetcaulem  24497  iscmet3lem1  24500  bcthlem4  24536  ovollb2lem  24697  ovolicc2lem3  24728  voliunlem3  24761  volcn  24815  itg10a  24920  itg1ge0a  24921  bddiblnc  25051  dvcnvrelem1  25226  dvfsumrlim  25240  itgsubst  25258  ulmcn  25603  ulmdvlem3  25606  mtest  25608  tanord  25739  emcllem6  26195  ftalem2  26268  chtub  26405  fsumvma2  26407  vmasum  26409  chpchtsum  26412  bcmono  26470  bclbnd  26473  bposlem1  26477  bposlem5  26481  bposlem6  26482  lgsne0  26528  gausslemma2dlem1a  26558  chtppilim  26668  dchrisumlem3  26684  pntrsumbnd2  26760  pntlemf  26798  pntlem3  26802  pntleml  26804  upgr2pthnlp  28145  crctcshwlkn0lem3  28222  crctcshwlkn0lem5  28224  eupth2lems  28647  grpoidinvlem3  28913  grpoideu  28916  vacn  29101  blocni  29212  ubthlem2  29278  chscllem2  30045  lnconi  30440  pjnmopi  30555  atomli  30789  sumdmdlem2  30826  cdj3lem2b  30844  xraddge02  31124  fedgmullem1  31755  dfon2lem5  33808  dfon2lem6  33809  nosupno  33951  noinfno  33966  cgrcoml  34343  btwnconn2  34449  fvineqsneq  35627  pibt2  35632  ltflcei  35809  poimirlem2  35823  poimirlem18  35839  poimirlem22  35843  poimirlem23  35844  poimirlem26  35847  poimirlem29  35850  poimirlem30  35851  poimirlem32  35853  heicant  35856  mblfinlem3  35860  mblfinlem4  35861  itg2addnclem  35872  itg2addnc  35875  ftc1anclem6  35899  ftc1anc  35902  mettrifi  35959  geomcau  35961  equivbnd  35992  heibor1lem  36011  bfplem1  36024  bfplem2  36025  rrncmslem  36034  divrngidl  36230  lecmtN  37312  cvrletrN  37329  llnnleat  37569  lplnnle2at  37597  lvolnle3at  37638  dalem21  37750  cdlemblem  37849  osumcllem11N  38022  pexmidlem8N  38033  lhpmcvr4N  38082  cdleme32b  38498  cdleme35fnpq  38505  cdleme48bw  38558  cdlemf1  38617  cdlemg2fv2  38656  cdlemg7fvbwN  38663  cdlemg27b  38752  tendoeq2  38830  dia2dimlem1  39120  dihord6apre  39312  dihord5apre  39318  dihglbcpreN  39356  dochnel2  39448  dihjat1lem  39484  dochexmidlem8  39523  mapdordlem2  39693  3cubeslem1  40543  iscard5  41181  frege124d  41407  mnringmulrcld  41884  climinf  43196  2ffzoeq  44878  iccpartlt  44934  lighneallem2  45116  bgoldbtbndlem3  45317  bgoldbtbndlem4  45318  tgoldbach  45327  fllog2  45972  dignn0ldlem  46006