Theorem mpand 683

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

Syntax hints:   → wi 4   ∧ wa 387

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 199  df-an 388

This theorem is referenced by:  mpani  684  mp2and  687  ecase2d  1013  disjss3  4925  sotri2  5827  fpropnf1  6849  ovig  7111  orduniorsuc  7360  omopth2  8010  frfi  8557  ordunifi  8562  finsschain  8625  cantnfp1lem3  8936  cantnfp1  8937  p1le  11285  nnge1  11467  zltp1le  11844  gtndiv  11871  uzss  12078  eluzadd  12086  uzm1  12089  addlelt  12319  xrre2  12379  xrre3  12380  xrmaxlt  12390  xrmaxle  12392  xrsupsslem  12515  xrub  12520  supxrunb1  12527  zltaddlt1le  12705  nn0p1elfzo  12894  elfzoext  12908  flflp1  12991  ceile  13031  modfzo0difsn  13125  seqf1olem1  13223  leexp2r  13352  expnlbnd2  13409  facavg  13475  wrdred1hash  13723  ccat2s1fvw  13800  caubnd2  14577  limsupbnd1  14699  limsupbnd2  14700  rlim2lt  14714  rlim3  14715  o1co  14803  mulcn2  14812  cn1lem  14814  rlimo1  14833  climsqz  14857  climsqz2  14858  rlimsqzlem  14865  lo1le  14868  rlimno1  14870  climsup  14886  caucvgrlem2  14891  iseraltlem2  14899  iseralt  14901  fsumabs  15015  cvgcmp  15030  cvgcmpce  15032  isumltss  15062  cvgrat  15098  ruclem9  15450  ruclem12  15453  bitsfzolem  15642  bitsfzo  15643  sadcaddlem  15665  gcdzeq  15757  algcvgblem  15776  algcvga  15778  lcmdvdsb  15812  lcmftp  15835  coprm  15910  eulerthlem2  15974  pclem  16030  infpn2  16104  prmreclem1  16107  prmreclem4  16110  ramtlecl  16191  prmgaplem7  16248  initoeu2  17147  lubval  17465  lublecllem  17469  glbval  17478  joinle  17495  latmlem1  17562  odmulg  18457  efginvrel2  18624  pgpfac1lem5  18964  chfacfscmul0  21186  chfacfpmmul0  21190  1stccnp  21790  qustgplem  22448  imasdsf1olem  22702  bldisj  22727  xbln0  22743  prdsbl  22820  metss2lem  22840  stdbdxmet  22844  ngptgp  22964  nghmcn  23073  icoopnst  23262  iocopnst  23263  cnllycmp  23279  iscau3  23600  cmetcaulem  23610  iscmet3lem1  23613  bcthlem4  23649  ovollb2lem  23808  ovolicc2lem3  23839  voliunlem3  23872  volcn  23926  itg10a  24030  itg1ge0a  24031  dvcnvrelem1  24333  dvfsumrlim  24347  itgsubst  24365  ulmcn  24706  ulmdvlem3  24709  mtest  24711  tanord  24839  emcllem6  25296  ftalem2  25369  chtub  25506  fsumvma2  25508  vmasum  25510  chpchtsum  25513  bcmono  25571  bclbnd  25574  bposlem1  25578  bposlem5  25582  bposlem6  25583  lgsne0  25629  gausslemma2dlem1a  25659  chtppilim  25769  dchrisumlem3  25785  pntrsumbnd2  25861  pntlemf  25899  pntlem3  25903  pntleml  25905  upgr2pthnlp  27237  crctcshwlkn0lem3  27314  crctcshwlkn0lem5  27316  eupth2lems  27784  grpoidinvlem3  28076  grpoideu  28079  vacn  28264  blocni  28375  ubthlem2  28442  chscllem2  29212  lnconi  29607  pjnmopi  29722  atomli  29956  sumdmdlem2  29993  cdj3lem2b  30011  xraddge02  30257  fedgmullem1  30687  dfon2lem5  32585  dfon2lem6  32586  nosupno  32757  cgrcoml  33011  btwnconn2  33117  fvineqsneq  34167  pibt2  34172  ltflcei  34354  poimirlem2  34368  poimirlem18  34384  poimirlem22  34388  poimirlem23  34389  poimirlem26  34392  poimirlem29  34395  poimirlem30  34396  poimirlem32  34398  heicant  34401  mblfinlem3  34405  mblfinlem4  34406  itg2addnclem  34417  itg2addnc  34420  bddiblnc  34436  ftc1anclem6  34446  ftc1anc  34449  mettrifi  34507  geomcau  34509  equivbnd  34543  heibor1lem  34562  bfplem1  34575  bfplem2  34576  rrncmslem  34585  divrngidl  34781  lecmtN  35870  cvrletrN  35887  llnnleat  36127  lplnnle2at  36155  lvolnle3at  36196  dalem21  36308  cdlemblem  36407  osumcllem11N  36580  pexmidlem8N  36591  lhpmcvr4N  36640  cdleme32b  37056  cdleme35fnpq  37063  cdleme48bw  37116  cdlemf1  37175  cdlemg2fv2  37214  cdlemg7fvbwN  37221  cdlemg27b  37310  tendoeq2  37388  dia2dimlem1  37678  dihord6apre  37870  dihord5apre  37876  dihglbcpreN  37914  dochnel2  38006  dihjat1lem  38042  dochexmidlem8  38081  mapdordlem2  38251  frege124d  39503  climinf  41348  2ffzoeq  42964  iccpartlt  42986  lighneallem2  43169  bgoldbtbndlem3  43370  bgoldbtbndlem4  43371  tgoldbach  43380  fllog2  44026  dignn0ldlem  44060