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  5118  sotri2  6118  fpropnf1  7259  ovig  7551  orduniorsuc  7822  resf1ext2b  7929  omopth2  8594  onomeneq  9235  frfi  9291  ordunifi  9296  finsschain  9369  cantnfp1lem3  9692  cantnfp1  9693  p1le  12084  nnge1  12266  zltp1le  12640  gtndiv  12668  uzss  12873  eluzaddOLD  12885  uzm1  12888  addlelt  13121  xrre2  13184  xrre3  13185  xrmaxlt  13195  xrmaxle  13197  xrsupsslem  13321  xrub  13326  supxrunb1  13333  zltaddlt1le  13520  nn0p1elfzo  13717  flflp1  13822  ceile  13864  modfzo0difsn  13959  seqf1olem1  14057  leexp2r  14190  expnlbnd2  14250  facavg  14317  wrdred1hash  14577  ccat2s1fvw  14654  caubnd2  15374  limsupbnd1  15496  limsupbnd2  15497  rlim2lt  15511  rlim3  15512  o1co  15600  mulcn2  15610  cn1lem  15612  rlimo1  15631  climsqz  15655  climsqz2  15656  rlimsqzlem  15663  lo1le  15666  rlimno1  15668  climsup  15684  caucvgrlem2  15689  iseraltlem2  15697  iseralt  15699  fsumabs  15815  cvgcmp  15830  cvgcmpce  15832  isumltss  15862  cvgrat  15897  ruclem9  16254  ruclem12  16257  bitsfzolem  16451  bitsfzo  16452  sadcaddlem  16474  gcdzeq  16569  algcvgblem  16594  algcvga  16596  lcmdvdsb  16630  lcmftp  16653  coprm  16728  eulerthlem2  16799  pclem  16856  infpn2  16931  prmreclem1  16934  prmreclem4  16937  ramtlecl  17018  prmgaplem7  17075  initoeu2  18027  lubval  18364  lublecllem  18368  glbval  18377  joinle  18394  latmlem1  18477  odmulg  19535  efginvrel2  19706  pgpfac1lem5  20060  chfacfscmul0  22794  chfacfpmmul0  22798  1stccnp  23398  qustgplem  24057  imasdsf1olem  24310  bldisj  24335  xbln0  24351  prdsbl  24428  metss2lem  24448  stdbdxmet  24452  ngptgp  24573  nghmcn  24682  icoopnst  24885  iocopnst  24886  cnllycmp  24904  iscau3  25228  cmetcaulem  25238  iscmet3lem1  25241  bcthlem4  25277  ovollb2lem  25439  ovolicc2lem3  25470  voliunlem3  25503  volcn  25557  itg10a  25661  itg1ge0a  25662  bddiblnc  25793  dvcnvrelem1  25972  dvfsumrlim  25988  itgsubst  26006  ulmcn  26358  ulmdvlem3  26361  mtest  26363  tanord  26497  emcllem6  26961  ftalem2  27034  chtub  27173  fsumvma2  27175  vmasum  27177  chpchtsum  27180  bcmono  27238  bclbnd  27241  bposlem1  27245  bposlem5  27249  bposlem6  27250  lgsne0  27296  gausslemma2dlem1a  27326  chtppilim  27436  dchrisumlem3  27452  pntrsumbnd2  27528  pntlemf  27566  pntlem3  27570  pntleml  27572  nosupno  27665  noinfno  27680  mulsproplem6  28064  mulsproplem7  28065  upgr2pthnlp  29660  crctcshwlkn0lem3  29740  crctcshwlkn0lem5  29742  eupth2lems  30165  grpoidinvlem3  30433  grpoideu  30436  vacn  30621  blocni  30732  ubthlem2  30798  chscllem2  31565  lnconi  31960  pjnmopi  32075  atomli  32309  sumdmdlem2  32346  cdj3lem2b  32364  xraddge02  32680  fedgmullem1  33615  dfon2lem5  35751  dfon2lem6  35752  cgrcoml  35960  btwnconn2  36066  fvineqsneq  37376  pibt2  37381  ltflcei  37578  poimirlem2  37592  poimirlem18  37608  poimirlem22  37612  poimirlem23  37613  poimirlem26  37616  poimirlem29  37619  poimirlem30  37620  poimirlem32  37622  heicant  37625  mblfinlem3  37629  mblfinlem4  37630  itg2addnclem  37641  itg2addnc  37644  ftc1anclem6  37668  ftc1anc  37671  mettrifi  37727  geomcau  37729  equivbnd  37760  heibor1lem  37779  bfplem1  37792  bfplem2  37793  rrncmslem  37802  divrngidl  37998  lecmtN  39220  cvrletrN  39237  llnnleat  39478  lplnnle2at  39506  lvolnle3at  39547  dalem21  39659  cdlemblem  39758  osumcllem11N  39931  pexmidlem8N  39942  lhpmcvr4N  39991  cdleme32b  40407  cdleme35fnpq  40414  cdleme48bw  40467  cdlemf1  40526  cdlemg2fv2  40565  cdlemg7fvbwN  40572  cdlemg27b  40661  tendoeq2  40739  dia2dimlem1  41029  dihord6apre  41221  dihord5apre  41227  dihglbcpreN  41265  dochnel2  41357  dihjat1lem  41393  dochexmidlem8  41432  mapdordlem2  41602  eqresfnbd  42230  3cubeslem1  42654  ordnexbtwnsuc  43238  naddcnfid2  43339  nadd2rabex  43357  iscard5  43507  frege124d  43732  mnringmulrcld  44200  climinf  45583  2ffzoeq  47304  iccpartlt  47386  lighneallem2  47568  bgoldbtbndlem3  47769  bgoldbtbndlem4  47770  tgoldbach  47779  fllog2  48496  dignn0ldlem  48530