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  5088  sotri2  6073  fpropnf1  7196  ovig  7487  orduniorsuc  7755  resf1ext2b  7860  omopth2  8494  onomeneq  9118  frfi  9164  ordunifi  9169  finsschain  9238  cantnfp1lem3  9565  cantnfp1  9566  p1le  11958  nnge1  12145  zltp1le  12514  gtndiv  12542  uzss  12747  eluzaddOLD  12759  uzm1  12762  addlelt  12998  xrre2  13061  xrre3  13062  xrmaxlt  13072  xrmaxle  13074  xrsupsslem  13198  xrub  13203  supxrunb1  13210  zltaddlt1le  13397  nn0p1elfzo  13594  flflp1  13703  ceile  13745  modfzo0difsn  13842  seqf1olem1  13940  leexp2r  14073  expnlbnd2  14133  facavg  14200  wrdred1hash  14460  ccat2s1fvw  14538  caubnd2  15257  limsupbnd1  15381  limsupbnd2  15382  rlim2lt  15396  rlim3  15397  o1co  15485  mulcn2  15495  cn1lem  15497  rlimo1  15516  climsqz  15540  climsqz2  15541  rlimsqzlem  15548  lo1le  15551  rlimno1  15553  climsup  15569  caucvgrlem2  15574  iseraltlem2  15582  iseralt  15584  fsumabs  15700  cvgcmp  15715  cvgcmpce  15717  isumltss  15747  cvgrat  15782  ruclem9  16139  ruclem12  16142  bitsfzolem  16337  bitsfzo  16338  sadcaddlem  16360  gcdzeq  16455  algcvgblem  16480  algcvga  16482  lcmdvdsb  16516  lcmftp  16539  coprm  16614  eulerthlem2  16685  pclem  16742  infpn2  16817  prmreclem1  16820  prmreclem4  16823  ramtlecl  16904  prmgaplem7  16961  initoeu2  17915  lubval  18252  lublecllem  18256  glbval  18265  joinle  18282  latmlem1  18367  odmulg  19461  efginvrel2  19632  pgpfac1lem5  19986  chfacfscmul0  22766  chfacfpmmul0  22770  1stccnp  23370  qustgplem  24029  imasdsf1olem  24281  bldisj  24306  xbln0  24322  prdsbl  24399  metss2lem  24419  stdbdxmet  24423  ngptgp  24544  nghmcn  24653  icoopnst  24856  iocopnst  24857  cnllycmp  24875  iscau3  25198  cmetcaulem  25208  iscmet3lem1  25211  bcthlem4  25247  ovollb2lem  25409  ovolicc2lem3  25440  voliunlem3  25473  volcn  25527  itg10a  25631  itg1ge0a  25632  bddiblnc  25763  dvcnvrelem1  25942  dvfsumrlim  25958  itgsubst  25976  ulmcn  26328  ulmdvlem3  26331  mtest  26333  tanord  26467  emcllem6  26931  ftalem2  27004  chtub  27143  fsumvma2  27145  vmasum  27147  chpchtsum  27150  bcmono  27208  bclbnd  27211  bposlem1  27215  bposlem5  27219  bposlem6  27220  lgsne0  27266  gausslemma2dlem1a  27296  chtppilim  27406  dchrisumlem3  27422  pntrsumbnd2  27498  pntlemf  27536  pntlem3  27540  pntleml  27542  nosupno  27635  noinfno  27650  mulsproplem6  28053  mulsproplem7  28054  upgr2pthnlp  29703  crctcshwlkn0lem3  29783  crctcshwlkn0lem5  29785  eupth2lems  30208  grpoidinvlem3  30476  grpoideu  30479  vacn  30664  blocni  30775  ubthlem2  30841  chscllem2  31608  lnconi  32003  pjnmopi  32118  atomli  32352  sumdmdlem2  32389  cdj3lem2b  32407  xraddge02  32730  fedgmullem1  33632  dfon2lem5  35800  dfon2lem6  35801  cgrcoml  36009  btwnconn2  36115  fvineqsneq  37425  pibt2  37430  ltflcei  37627  poimirlem2  37641  poimirlem18  37657  poimirlem22  37661  poimirlem23  37662  poimirlem26  37665  poimirlem29  37668  poimirlem30  37669  poimirlem32  37671  heicant  37674  mblfinlem3  37678  mblfinlem4  37679  itg2addnclem  37690  itg2addnc  37693  ftc1anclem6  37717  ftc1anc  37720  mettrifi  37776  geomcau  37778  equivbnd  37809  heibor1lem  37828  bfplem1  37841  bfplem2  37842  rrncmslem  37851  divrngidl  38047  lecmtN  39274  cvrletrN  39291  llnnleat  39531  lplnnle2at  39559  lvolnle3at  39600  dalem21  39712  cdlemblem  39811  osumcllem11N  39984  pexmidlem8N  39995  lhpmcvr4N  40044  cdleme32b  40460  cdleme35fnpq  40467  cdleme48bw  40520  cdlemf1  40579  cdlemg2fv2  40618  cdlemg7fvbwN  40625  cdlemg27b  40714  tendoeq2  40792  dia2dimlem1  41082  dihord6apre  41274  dihord5apre  41280  dihglbcpreN  41318  dochnel2  41410  dihjat1lem  41446  dochexmidlem8  41485  mapdordlem2  41655  eqresfnbd  42244  3cubeslem1  42696  ordnexbtwnsuc  43279  naddcnfid2  43380  nadd2rabex  43398  iscard5  43548  frege124d  43773  mnringmulrcld  44240  climinf  45625  2ffzoeq  47337  iccpartlt  47434  lighneallem2  47616  bgoldbtbndlem3  47817  bgoldbtbndlem4  47818  tgoldbach  47827  fllog2  48579  dignn0ldlem  48613