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

Syntax hints:   → wi 4   ∧ wa 394

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 395

This theorem is referenced by:  mpani  694  mp2and  697  ecase2dOLD  1028  disjss3  5147  sotri2  6135  fpropnf1  7275  ovig  7565  orduniorsuc  7832  omopth2  8603  onomeneq  9251  frfi  9311  ordunifi  9316  finsschain  9383  cantnfp1lem3  9703  cantnfp1  9704  p1le  12089  nnge1  12270  zltp1le  12642  gtndiv  12669  uzss  12875  eluzaddOLD  12887  uzm1  12890  addlelt  13120  xrre2  13181  xrre3  13182  xrmaxlt  13192  xrmaxle  13194  xrsupsslem  13318  xrub  13323  supxrunb1  13330  zltaddlt1le  13514  nn0p1elfzo  13707  elfzoext  13721  flflp1  13804  ceile  13846  modfzo0difsn  13940  seqf1olem1  14038  leexp2r  14170  expnlbnd2  14228  facavg  14292  wrdred1hash  14543  ccat2s1fvw  14620  caubnd2  15336  limsupbnd1  15458  limsupbnd2  15459  rlim2lt  15473  rlim3  15474  o1co  15562  mulcn2  15572  cn1lem  15574  rlimo1  15593  climsqz  15617  climsqz2  15618  rlimsqzlem  15627  lo1le  15630  rlimno1  15632  climsup  15648  caucvgrlem2  15653  iseraltlem2  15661  iseralt  15663  fsumabs  15779  cvgcmp  15794  cvgcmpce  15796  isumltss  15826  cvgrat  15861  ruclem9  16214  ruclem12  16217  bitsfzolem  16408  bitsfzo  16409  sadcaddlem  16431  gcdzeq  16527  algcvgblem  16547  algcvga  16549  lcmdvdsb  16583  lcmftp  16606  coprm  16681  eulerthlem2  16750  pclem  16806  infpn2  16881  prmreclem1  16884  prmreclem4  16887  ramtlecl  16968  prmgaplem7  17025  initoeu2  18004  lubval  18347  lublecllem  18351  glbval  18360  joinle  18377  latmlem1  18460  odmulg  19515  efginvrel2  19686  pgpfac1lem5  20040  chfacfscmul0  22790  chfacfpmmul0  22794  1stccnp  23396  qustgplem  24055  imasdsf1olem  24309  bldisj  24334  xbln0  24350  prdsbl  24430  metss2lem  24450  stdbdxmet  24454  ngptgp  24575  nghmcn  24692  icoopnst  24893  iocopnst  24894  cnllycmp  24912  iscau3  25236  cmetcaulem  25246  iscmet3lem1  25249  bcthlem4  25285  ovollb2lem  25447  ovolicc2lem3  25478  voliunlem3  25511  volcn  25565  itg10a  25670  itg1ge0a  25671  bddiblnc  25801  dvcnvrelem1  25980  dvfsumrlim  25996  itgsubst  26014  ulmcn  26365  ulmdvlem3  26368  mtest  26370  tanord  26502  emcllem6  26963  ftalem2  27036  chtub  27175  fsumvma2  27177  vmasum  27179  chpchtsum  27182  bcmono  27240  bclbnd  27243  bposlem1  27247  bposlem5  27251  bposlem6  27252  lgsne0  27298  gausslemma2dlem1a  27328  chtppilim  27438  dchrisumlem3  27454  pntrsumbnd2  27530  pntlemf  27568  pntlem3  27572  pntleml  27574  nosupno  27666  noinfno  27681  mulsproplem6  28055  mulsproplem7  28056  upgr2pthnlp  29602  crctcshwlkn0lem3  29679  crctcshwlkn0lem5  29681  eupth2lems  30104  grpoidinvlem3  30372  grpoideu  30375  vacn  30560  blocni  30671  ubthlem2  30737  chscllem2  31504  lnconi  31899  pjnmopi  32014  atomli  32248  sumdmdlem2  32285  cdj3lem2b  32303  xraddge02  32583  fedgmullem1  33397  dfon2lem5  35453  dfon2lem6  35454  cgrcoml  35662  btwnconn2  35768  fvineqsneq  36961  pibt2  36966  ltflcei  37151  poimirlem2  37165  poimirlem18  37181  poimirlem22  37185  poimirlem23  37186  poimirlem26  37189  poimirlem29  37192  poimirlem30  37193  poimirlem32  37195  heicant  37198  mblfinlem3  37202  mblfinlem4  37203  itg2addnclem  37214  itg2addnc  37217  ftc1anclem6  37241  ftc1anc  37244  mettrifi  37300  geomcau  37302  equivbnd  37333  heibor1lem  37352  bfplem1  37365  bfplem2  37366  rrncmslem  37375  divrngidl  37571  lecmtN  38797  cvrletrN  38814  llnnleat  39055  lplnnle2at  39083  lvolnle3at  39124  dalem21  39236  cdlemblem  39335  osumcllem11N  39508  pexmidlem8N  39519  lhpmcvr4N  39568  cdleme32b  39984  cdleme35fnpq  39991  cdleme48bw  40044  cdlemf1  40103  cdlemg2fv2  40142  cdlemg7fvbwN  40149  cdlemg27b  40238  tendoeq2  40316  dia2dimlem1  40606  dihord6apre  40798  dihord5apre  40804  dihglbcpreN  40842  dochnel2  40934  dihjat1lem  40970  dochexmidlem8  41009  mapdordlem2  41179  eqresfnbd  41791  3cubeslem1  42169  ordnexbtwnsuc  42761  naddcnfid2  42862  nadd2rabex  42880  iscard5  43031  frege124d  43256  mnringmulrcld  43730  climinf  45057  2ffzoeq  46771  iccpartlt  46827  lighneallem2  47009  bgoldbtbndlem3  47210  bgoldbtbndlem4  47211  tgoldbach  47220  fllog2  47753  dignn0ldlem  47787