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  5106  sotri2  6102  fpropnf1  7242  ovig  7535  orduniorsuc  7805  resf1ext2b  7911  omopth2  8548  onomeneq  9178  frfi  9232  ordunifi  9237  finsschain  9310  cantnfp1lem3  9633  cantnfp1  9634  p1le  12027  nnge1  12214  zltp1le  12583  gtndiv  12611  uzss  12816  eluzaddOLD  12828  uzm1  12831  addlelt  13067  xrre2  13130  xrre3  13131  xrmaxlt  13141  xrmaxle  13143  xrsupsslem  13267  xrub  13272  supxrunb1  13279  zltaddlt1le  13466  nn0p1elfzo  13663  flflp1  13769  ceile  13811  modfzo0difsn  13908  seqf1olem1  14006  leexp2r  14139  expnlbnd2  14199  facavg  14266  wrdred1hash  14526  ccat2s1fvw  14603  caubnd2  15324  limsupbnd1  15448  limsupbnd2  15449  rlim2lt  15463  rlim3  15464  o1co  15552  mulcn2  15562  cn1lem  15564  rlimo1  15583  climsqz  15607  climsqz2  15608  rlimsqzlem  15615  lo1le  15618  rlimno1  15620  climsup  15636  caucvgrlem2  15641  iseraltlem2  15649  iseralt  15651  fsumabs  15767  cvgcmp  15782  cvgcmpce  15784  isumltss  15814  cvgrat  15849  ruclem9  16206  ruclem12  16209  bitsfzolem  16404  bitsfzo  16405  sadcaddlem  16427  gcdzeq  16522  algcvgblem  16547  algcvga  16549  lcmdvdsb  16583  lcmftp  16606  coprm  16681  eulerthlem2  16752  pclem  16809  infpn2  16884  prmreclem1  16887  prmreclem4  16890  ramtlecl  16971  prmgaplem7  17028  initoeu2  17978  lubval  18315  lublecllem  18319  glbval  18328  joinle  18345  latmlem1  18428  odmulg  19486  efginvrel2  19657  pgpfac1lem5  20011  chfacfscmul0  22745  chfacfpmmul0  22749  1stccnp  23349  qustgplem  24008  imasdsf1olem  24261  bldisj  24286  xbln0  24302  prdsbl  24379  metss2lem  24399  stdbdxmet  24403  ngptgp  24524  nghmcn  24633  icoopnst  24836  iocopnst  24837  cnllycmp  24855  iscau3  25178  cmetcaulem  25188  iscmet3lem1  25191  bcthlem4  25227  ovollb2lem  25389  ovolicc2lem3  25420  voliunlem3  25453  volcn  25507  itg10a  25611  itg1ge0a  25612  bddiblnc  25743  dvcnvrelem1  25922  dvfsumrlim  25938  itgsubst  25956  ulmcn  26308  ulmdvlem3  26311  mtest  26313  tanord  26447  emcllem6  26911  ftalem2  26984  chtub  27123  fsumvma2  27125  vmasum  27127  chpchtsum  27130  bcmono  27188  bclbnd  27191  bposlem1  27195  bposlem5  27199  bposlem6  27200  lgsne0  27246  gausslemma2dlem1a  27276  chtppilim  27386  dchrisumlem3  27402  pntrsumbnd2  27478  pntlemf  27516  pntlem3  27520  pntleml  27522  nosupno  27615  noinfno  27630  mulsproplem6  28024  mulsproplem7  28025  upgr2pthnlp  29662  crctcshwlkn0lem3  29742  crctcshwlkn0lem5  29744  eupth2lems  30167  grpoidinvlem3  30435  grpoideu  30438  vacn  30623  blocni  30734  ubthlem2  30800  chscllem2  31567  lnconi  31962  pjnmopi  32077  atomli  32311  sumdmdlem2  32348  cdj3lem2b  32366  xraddge02  32680  fedgmullem1  33625  dfon2lem5  35775  dfon2lem6  35776  cgrcoml  35984  btwnconn2  36090  fvineqsneq  37400  pibt2  37405  ltflcei  37602  poimirlem2  37616  poimirlem18  37632  poimirlem22  37636  poimirlem23  37637  poimirlem26  37640  poimirlem29  37643  poimirlem30  37644  poimirlem32  37646  heicant  37649  mblfinlem3  37653  mblfinlem4  37654  itg2addnclem  37665  itg2addnc  37668  ftc1anclem6  37692  ftc1anc  37695  mettrifi  37751  geomcau  37753  equivbnd  37784  heibor1lem  37803  bfplem1  37816  bfplem2  37817  rrncmslem  37826  divrngidl  38022  lecmtN  39249  cvrletrN  39266  llnnleat  39507  lplnnle2at  39535  lvolnle3at  39576  dalem21  39688  cdlemblem  39787  osumcllem11N  39960  pexmidlem8N  39971  lhpmcvr4N  40020  cdleme32b  40436  cdleme35fnpq  40443  cdleme48bw  40496  cdlemf1  40555  cdlemg2fv2  40594  cdlemg7fvbwN  40601  cdlemg27b  40690  tendoeq2  40768  dia2dimlem1  41058  dihord6apre  41250  dihord5apre  41256  dihglbcpreN  41294  dochnel2  41386  dihjat1lem  41422  dochexmidlem8  41461  mapdordlem2  41631  eqresfnbd  42220  3cubeslem1  42672  ordnexbtwnsuc  43256  naddcnfid2  43357  nadd2rabex  43375  iscard5  43525  frege124d  43750  mnringmulrcld  44217  climinf  45604  2ffzoeq  47328  iccpartlt  47425  lighneallem2  47607  bgoldbtbndlem3  47808  bgoldbtbndlem4  47809  tgoldbach  47818  fllog2  48557  dignn0ldlem  48591