Theorem mpand 694

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

Syntax hints:   → wi 4   ∧ wa 395

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 396

This theorem is referenced by:  mpani  695  mp2and  698  ecase2dOLD  1029  disjss3  5141  sotri2  6129  fpropnf1  7271  ovig  7561  orduniorsuc  7827  omopth2  8598  onomeneq  9244  frfi  9304  ordunifi  9309  finsschain  9375  cantnfp1lem3  9695  cantnfp1  9696  p1le  12081  nnge1  12262  zltp1le  12634  gtndiv  12661  uzss  12867  eluzaddOLD  12879  uzm1  12882  addlelt  13112  xrre2  13173  xrre3  13174  xrmaxlt  13184  xrmaxle  13186  xrsupsslem  13310  xrub  13315  supxrunb1  13322  zltaddlt1le  13506  nn0p1elfzo  13699  elfzoext  13713  flflp1  13796  ceile  13838  modfzo0difsn  13932  seqf1olem1  14030  leexp2r  14162  expnlbnd2  14220  facavg  14284  wrdred1hash  14535  ccat2s1fvw  14612  caubnd2  15328  limsupbnd1  15450  limsupbnd2  15451  rlim2lt  15465  rlim3  15466  o1co  15554  mulcn2  15564  cn1lem  15566  rlimo1  15585  climsqz  15609  climsqz2  15610  rlimsqzlem  15619  lo1le  15622  rlimno1  15624  climsup  15640  caucvgrlem2  15645  iseraltlem2  15653  iseralt  15655  fsumabs  15771  cvgcmp  15786  cvgcmpce  15788  isumltss  15818  cvgrat  15853  ruclem9  16206  ruclem12  16209  bitsfzolem  16400  bitsfzo  16401  sadcaddlem  16423  gcdzeq  16519  algcvgblem  16539  algcvga  16541  lcmdvdsb  16575  lcmftp  16598  coprm  16673  eulerthlem2  16742  pclem  16798  infpn2  16873  prmreclem1  16876  prmreclem4  16879  ramtlecl  16960  prmgaplem7  17017  initoeu2  17996  lubval  18339  lublecllem  18343  glbval  18352  joinle  18369  latmlem1  18452  odmulg  19502  efginvrel2  19673  pgpfac1lem5  20027  chfacfscmul0  22747  chfacfpmmul0  22751  1stccnp  23353  qustgplem  24012  imasdsf1olem  24266  bldisj  24291  xbln0  24307  prdsbl  24387  metss2lem  24407  stdbdxmet  24411  ngptgp  24532  nghmcn  24649  icoopnst  24850  iocopnst  24851  cnllycmp  24869  iscau3  25193  cmetcaulem  25203  iscmet3lem1  25206  bcthlem4  25242  ovollb2lem  25404  ovolicc2lem3  25435  voliunlem3  25468  volcn  25522  itg10a  25627  itg1ge0a  25628  bddiblnc  25758  dvcnvrelem1  25937  dvfsumrlim  25953  itgsubst  25971  ulmcn  26322  ulmdvlem3  26325  mtest  26327  tanord  26459  emcllem6  26920  ftalem2  26993  chtub  27132  fsumvma2  27134  vmasum  27136  chpchtsum  27139  bcmono  27197  bclbnd  27200  bposlem1  27204  bposlem5  27208  bposlem6  27209  lgsne0  27255  gausslemma2dlem1a  27285  chtppilim  27395  dchrisumlem3  27411  pntrsumbnd2  27487  pntlemf  27525  pntlem3  27529  pntleml  27531  nosupno  27623  noinfno  27638  mulsproplem6  28008  mulsproplem7  28009  upgr2pthnlp  29533  crctcshwlkn0lem3  29610  crctcshwlkn0lem5  29612  eupth2lems  30035  grpoidinvlem3  30303  grpoideu  30306  vacn  30491  blocni  30602  ubthlem2  30668  chscllem2  31435  lnconi  31830  pjnmopi  31945  atomli  32179  sumdmdlem2  32216  cdj3lem2b  32234  xraddge02  32510  fedgmullem1  33259  dfon2lem5  35319  dfon2lem6  35320  cgrcoml  35528  btwnconn2  35634  fvineqsneq  36827  pibt2  36832  ltflcei  37016  poimirlem2  37030  poimirlem18  37046  poimirlem22  37050  poimirlem23  37051  poimirlem26  37054  poimirlem29  37057  poimirlem30  37058  poimirlem32  37060  heicant  37063  mblfinlem3  37067  mblfinlem4  37068  itg2addnclem  37079  itg2addnc  37082  ftc1anclem6  37106  ftc1anc  37109  mettrifi  37165  geomcau  37167  equivbnd  37198  heibor1lem  37217  bfplem1  37230  bfplem2  37231  rrncmslem  37240  divrngidl  37436  lecmtN  38665  cvrletrN  38682  llnnleat  38923  lplnnle2at  38951  lvolnle3at  38992  dalem21  39104  cdlemblem  39203  osumcllem11N  39376  pexmidlem8N  39387  lhpmcvr4N  39436  cdleme32b  39852  cdleme35fnpq  39859  cdleme48bw  39912  cdlemf1  39971  cdlemg2fv2  40010  cdlemg7fvbwN  40017  cdlemg27b  40106  tendoeq2  40184  dia2dimlem1  40474  dihord6apre  40666  dihord5apre  40672  dihglbcpreN  40710  dochnel2  40802  dihjat1lem  40838  dochexmidlem8  40877  mapdordlem2  41047  eqresfnbd  41643  3cubeslem1  42026  ordnexbtwnsuc  42619  naddcnfid2  42720  nadd2rabex  42738  iscard5  42889  frege124d  43114  mnringmulrcld  43588  climinf  44917  2ffzoeq  46631  iccpartlt  46687  lighneallem2  46869  bgoldbtbndlem3  47070  bgoldbtbndlem4  47071  tgoldbach  47080  fllog2  47564  dignn0ldlem  47598