Theorem mpand 696

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 695	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 207  df-an 396

This theorem is referenced by:  mpani  697  mp2and  700  disjss3  5085  sotri2  6093  fpropnf1  7222  ovig  7513  orduniorsuc  7781  resf1ext2b  7886  omopth2  8519  onomeneq  9148  frfi  9195  ordunifi  9200  finsschain  9269  cantnfp1lem3  9601  cantnfp1  9602  p1le  12000  nnge1  12205  zltp1le  12577  gtndiv  12606  uzss  12811  uzm1  12822  addlelt  13058  xrre2  13122  xrre3  13123  xrmaxlt  13133  xrmaxle  13135  xrsupsslem  13259  xrub  13264  supxrunb1  13271  zltaddlt1le  13458  nn0p1elfzo  13657  flflp1  13766  ceile  13808  modfzo0difsn  13905  seqf1olem1  14003  leexp2r  14136  expnlbnd2  14196  facavg  14263  wrdred1hash  14523  ccat2s1fvw  14601  caubnd2  15320  limsupbnd1  15444  limsupbnd2  15445  rlim2lt  15459  rlim3  15460  o1co  15548  mulcn2  15558  cn1lem  15560  rlimo1  15579  climsqz  15603  climsqz2  15604  rlimsqzlem  15611  lo1le  15614  rlimno1  15616  climsup  15632  caucvgrlem2  15637  iseraltlem2  15645  iseralt  15647  fsumabs  15764  cvgcmp  15779  cvgcmpce  15781  isumltss  15813  cvgrat  15848  ruclem9  16205  ruclem12  16208  bitsfzolem  16403  bitsfzo  16404  sadcaddlem  16426  gcdzeq  16521  algcvgblem  16546  algcvga  16548  lcmdvdsb  16582  lcmftp  16605  coprm  16681  eulerthlem2  16752  pclem  16809  infpn2  16884  prmreclem1  16887  prmreclem4  16890  ramtlecl  16971  prmgaplem7  17028  initoeu2  17983  lubval  18320  lublecllem  18324  glbval  18333  joinle  18350  latmlem1  18435  odmulg  19531  efginvrel2  19702  pgpfac1lem5  20056  chfacfscmul0  22823  chfacfpmmul0  22827  1stccnp  23427  qustgplem  24086  imasdsf1olem  24338  bldisj  24363  xbln0  24379  prdsbl  24456  metss2lem  24476  stdbdxmet  24480  ngptgp  24601  nghmcn  24710  icoopnst  24906  iocopnst  24907  cnllycmp  24923  iscau3  25245  cmetcaulem  25255  iscmet3lem1  25258  bcthlem4  25294  ovollb2lem  25455  ovolicc2lem3  25486  voliunlem3  25519  volcn  25573  itg10a  25677  itg1ge0a  25678  bddiblnc  25809  dvcnvrelem1  25984  dvfsumrlim  25998  itgsubst  26016  ulmcn  26364  ulmdvlem3  26367  mtest  26369  tanord  26502  emcllem6  26964  ftalem2  27037  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  27667  noinfno  27682  mulsproplem6  28113  mulsproplem7  28114  upgr2pthnlp  29800  crctcshwlkn0lem3  29880  crctcshwlkn0lem5  29882  eupth2lems  30308  grpoidinvlem3  30577  grpoideu  30580  vacn  30765  blocni  30876  ubthlem2  30942  chscllem2  31709  lnconi  32104  pjnmopi  32219  atomli  32453  sumdmdlem2  32490  cdj3lem2b  32508  xraddge02  32830  fedgmullem1  33773  dfon2lem5  35967  dfon2lem6  35968  cgrcoml  36178  btwnconn2  36284  fvineqsneq  37728  pibt2  37733  ltflcei  37929  poimirlem2  37943  poimirlem18  37959  poimirlem22  37963  poimirlem23  37964  poimirlem26  37967  poimirlem29  37970  poimirlem30  37971  poimirlem32  37973  heicant  37976  mblfinlem3  37980  mblfinlem4  37981  itg2addnclem  37992  itg2addnc  37995  ftc1anclem6  38019  ftc1anc  38022  mettrifi  38078  geomcau  38080  equivbnd  38111  heibor1lem  38130  bfplem1  38143  bfplem2  38144  rrncmslem  38153  divrngidl  38349  preuniqval  38817  lecmtN  39702  cvrletrN  39719  llnnleat  39959  lplnnle2at  39987  lvolnle3at  40028  dalem21  40140  cdlemblem  40239  osumcllem11N  40412  pexmidlem8N  40423  lhpmcvr4N  40472  cdleme32b  40888  cdleme35fnpq  40895  cdleme48bw  40948  cdlemf1  41007  cdlemg2fv2  41046  cdlemg7fvbwN  41053  cdlemg27b  41142  tendoeq2  41220  dia2dimlem1  41510  dihord6apre  41702  dihord5apre  41708  dihglbcpreN  41746  dochnel2  41838  dihjat1lem  41874  dochexmidlem8  41913  mapdordlem2  42083  eqresfnbd  42673  3cubeslem1  43116  ordnexbtwnsuc  43695  naddcnfid2  43796  nadd2rabex  43814  iscard5  43963  frege124d  44188  mnringmulrcld  44655  climinf  46036  2ffzoeq  47770  iccpartlt  47878  lighneallem2  48063  bgoldbtbndlem3  48277  bgoldbtbndlem4  48278  tgoldbach  48287  fllog2  49038  dignn0ldlem  49072