Theorem mpand 695

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 694	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  696  mp2and  699  disjss3  5109  sotri2  6105  fpropnf1  7245  ovig  7538  orduniorsuc  7808  resf1ext2b  7914  omopth2  8551  onomeneq  9184  frfi  9239  ordunifi  9244  finsschain  9317  cantnfp1lem3  9640  cantnfp1  9641  p1le  12034  nnge1  12221  zltp1le  12590  gtndiv  12618  uzss  12823  eluzaddOLD  12835  uzm1  12838  addlelt  13074  xrre2  13137  xrre3  13138  xrmaxlt  13148  xrmaxle  13150  xrsupsslem  13274  xrub  13279  supxrunb1  13286  zltaddlt1le  13473  nn0p1elfzo  13670  flflp1  13776  ceile  13818  modfzo0difsn  13915  seqf1olem1  14013  leexp2r  14146  expnlbnd2  14206  facavg  14273  wrdred1hash  14533  ccat2s1fvw  14610  caubnd2  15331  limsupbnd1  15455  limsupbnd2  15456  rlim2lt  15470  rlim3  15471  o1co  15559  mulcn2  15569  cn1lem  15571  rlimo1  15590  climsqz  15614  climsqz2  15615  rlimsqzlem  15622  lo1le  15625  rlimno1  15627  climsup  15643  caucvgrlem2  15648  iseraltlem2  15656  iseralt  15658  fsumabs  15774  cvgcmp  15789  cvgcmpce  15791  isumltss  15821  cvgrat  15856  ruclem9  16213  ruclem12  16216  bitsfzolem  16411  bitsfzo  16412  sadcaddlem  16434  gcdzeq  16529  algcvgblem  16554  algcvga  16556  lcmdvdsb  16590  lcmftp  16613  coprm  16688  eulerthlem2  16759  pclem  16816  infpn2  16891  prmreclem1  16894  prmreclem4  16897  ramtlecl  16978  prmgaplem7  17035  initoeu2  17985  lubval  18322  lublecllem  18326  glbval  18335  joinle  18352  latmlem1  18435  odmulg  19493  efginvrel2  19664  pgpfac1lem5  20018  chfacfscmul0  22752  chfacfpmmul0  22756  1stccnp  23356  qustgplem  24015  imasdsf1olem  24268  bldisj  24293  xbln0  24309  prdsbl  24386  metss2lem  24406  stdbdxmet  24410  ngptgp  24531  nghmcn  24640  icoopnst  24843  iocopnst  24844  cnllycmp  24862  iscau3  25185  cmetcaulem  25195  iscmet3lem1  25198  bcthlem4  25234  ovollb2lem  25396  ovolicc2lem3  25427  voliunlem3  25460  volcn  25514  itg10a  25618  itg1ge0a  25619  bddiblnc  25750  dvcnvrelem1  25929  dvfsumrlim  25945  itgsubst  25963  ulmcn  26315  ulmdvlem3  26318  mtest  26320  tanord  26454  emcllem6  26918  ftalem2  26991  chtub  27130  fsumvma2  27132  vmasum  27134  chpchtsum  27137  bcmono  27195  bclbnd  27198  bposlem1  27202  bposlem5  27206  bposlem6  27207  lgsne0  27253  gausslemma2dlem1a  27283  chtppilim  27393  dchrisumlem3  27409  pntrsumbnd2  27485  pntlemf  27523  pntlem3  27527  pntleml  27529  nosupno  27622  noinfno  27637  mulsproplem6  28031  mulsproplem7  28032  upgr2pthnlp  29669  crctcshwlkn0lem3  29749  crctcshwlkn0lem5  29751  eupth2lems  30174  grpoidinvlem3  30442  grpoideu  30445  vacn  30630  blocni  30741  ubthlem2  30807  chscllem2  31574  lnconi  31969  pjnmopi  32084  atomli  32318  sumdmdlem2  32355  cdj3lem2b  32373  xraddge02  32687  fedgmullem1  33632  dfon2lem5  35782  dfon2lem6  35783  cgrcoml  35991  btwnconn2  36097  fvineqsneq  37407  pibt2  37412  ltflcei  37609  poimirlem2  37623  poimirlem18  37639  poimirlem22  37643  poimirlem23  37644  poimirlem26  37647  poimirlem29  37650  poimirlem30  37651  poimirlem32  37653  heicant  37656  mblfinlem3  37660  mblfinlem4  37661  itg2addnclem  37672  itg2addnc  37675  ftc1anclem6  37699  ftc1anc  37702  mettrifi  37758  geomcau  37760  equivbnd  37791  heibor1lem  37810  bfplem1  37823  bfplem2  37824  rrncmslem  37833  divrngidl  38029  lecmtN  39256  cvrletrN  39273  llnnleat  39514  lplnnle2at  39542  lvolnle3at  39583  dalem21  39695  cdlemblem  39794  osumcllem11N  39967  pexmidlem8N  39978  lhpmcvr4N  40027  cdleme32b  40443  cdleme35fnpq  40450  cdleme48bw  40503  cdlemf1  40562  cdlemg2fv2  40601  cdlemg7fvbwN  40608  cdlemg27b  40697  tendoeq2  40775  dia2dimlem1  41065  dihord6apre  41257  dihord5apre  41263  dihglbcpreN  41301  dochnel2  41393  dihjat1lem  41429  dochexmidlem8  41468  mapdordlem2  41638  eqresfnbd  42227  3cubeslem1  42679  ordnexbtwnsuc  43263  naddcnfid2  43364  nadd2rabex  43382  iscard5  43532  frege124d  43757  mnringmulrcld  44224  climinf  45611  2ffzoeq  47332  iccpartlt  47429  lighneallem2  47611  bgoldbtbndlem3  47812  bgoldbtbndlem4  47813  tgoldbach  47822  fllog2  48561  dignn0ldlem  48595