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  5092  sotri2  6081  fpropnf1  7207  ovig  7498  orduniorsuc  7766  resf1ext2b  7871  omopth2  8505  onomeneq  9129  frfi  9175  ordunifi  9180  finsschain  9249  cantnfp1lem3  9576  cantnfp1  9577  p1le  11972  nnge1  12159  zltp1le  12528  gtndiv  12556  uzss  12761  eluzaddOLD  12773  uzm1  12776  addlelt  13012  xrre2  13075  xrre3  13076  xrmaxlt  13086  xrmaxle  13088  xrsupsslem  13212  xrub  13217  supxrunb1  13224  zltaddlt1le  13411  nn0p1elfzo  13608  flflp1  13717  ceile  13759  modfzo0difsn  13856  seqf1olem1  13954  leexp2r  14087  expnlbnd2  14147  facavg  14214  wrdred1hash  14474  ccat2s1fvw  14552  caubnd2  15271  limsupbnd1  15395  limsupbnd2  15396  rlim2lt  15410  rlim3  15411  o1co  15499  mulcn2  15509  cn1lem  15511  rlimo1  15530  climsqz  15554  climsqz2  15555  rlimsqzlem  15562  lo1le  15565  rlimno1  15567  climsup  15583  caucvgrlem2  15588  iseraltlem2  15596  iseralt  15598  fsumabs  15714  cvgcmp  15729  cvgcmpce  15731  isumltss  15761  cvgrat  15796  ruclem9  16153  ruclem12  16156  bitsfzolem  16351  bitsfzo  16352  sadcaddlem  16374  gcdzeq  16469  algcvgblem  16494  algcvga  16496  lcmdvdsb  16530  lcmftp  16553  coprm  16628  eulerthlem2  16699  pclem  16756  infpn2  16831  prmreclem1  16834  prmreclem4  16837  ramtlecl  16918  prmgaplem7  16975  initoeu2  17929  lubval  18266  lublecllem  18270  glbval  18279  joinle  18296  latmlem1  18381  odmulg  19474  efginvrel2  19645  pgpfac1lem5  19999  chfacfscmul0  22779  chfacfpmmul0  22783  1stccnp  23383  qustgplem  24042  imasdsf1olem  24294  bldisj  24319  xbln0  24335  prdsbl  24412  metss2lem  24432  stdbdxmet  24436  ngptgp  24557  nghmcn  24666  icoopnst  24869  iocopnst  24870  cnllycmp  24888  iscau3  25211  cmetcaulem  25221  iscmet3lem1  25224  bcthlem4  25260  ovollb2lem  25422  ovolicc2lem3  25453  voliunlem3  25486  volcn  25540  itg10a  25644  itg1ge0a  25645  bddiblnc  25776  dvcnvrelem1  25955  dvfsumrlim  25971  itgsubst  25989  ulmcn  26341  ulmdvlem3  26344  mtest  26346  tanord  26480  emcllem6  26944  ftalem2  27017  chtub  27156  fsumvma2  27158  vmasum  27160  chpchtsum  27163  bcmono  27221  bclbnd  27224  bposlem1  27228  bposlem5  27232  bposlem6  27233  lgsne0  27279  gausslemma2dlem1a  27309  chtppilim  27419  dchrisumlem3  27435  pntrsumbnd2  27511  pntlemf  27549  pntlem3  27553  pntleml  27555  nosupno  27648  noinfno  27663  mulsproplem6  28066  mulsproplem7  28067  upgr2pthnlp  29717  crctcshwlkn0lem3  29797  crctcshwlkn0lem5  29799  eupth2lems  30225  grpoidinvlem3  30493  grpoideu  30496  vacn  30681  blocni  30792  ubthlem2  30858  chscllem2  31625  lnconi  32020  pjnmopi  32135  atomli  32369  sumdmdlem2  32406  cdj3lem2b  32424  xraddge02  32747  fedgmullem1  33649  dfon2lem5  35836  dfon2lem6  35837  cgrcoml  36047  btwnconn2  36153  fvineqsneq  37463  pibt2  37468  ltflcei  37654  poimirlem2  37668  poimirlem18  37684  poimirlem22  37688  poimirlem23  37689  poimirlem26  37692  poimirlem29  37695  poimirlem30  37696  poimirlem32  37698  heicant  37701  mblfinlem3  37705  mblfinlem4  37706  itg2addnclem  37717  itg2addnc  37720  ftc1anclem6  37744  ftc1anc  37747  mettrifi  37803  geomcau  37805  equivbnd  37836  heibor1lem  37855  bfplem1  37868  bfplem2  37869  rrncmslem  37878  divrngidl  38074  preuniqval  38514  lecmtN  39361  cvrletrN  39378  llnnleat  39618  lplnnle2at  39646  lvolnle3at  39687  dalem21  39799  cdlemblem  39898  osumcllem11N  40071  pexmidlem8N  40082  lhpmcvr4N  40131  cdleme32b  40547  cdleme35fnpq  40554  cdleme48bw  40607  cdlemf1  40666  cdlemg2fv2  40705  cdlemg7fvbwN  40712  cdlemg27b  40801  tendoeq2  40879  dia2dimlem1  41169  dihord6apre  41361  dihord5apre  41367  dihglbcpreN  41405  dochnel2  41497  dihjat1lem  41533  dochexmidlem8  41572  mapdordlem2  41742  eqresfnbd  42331  3cubeslem1  42782  ordnexbtwnsuc  43365  naddcnfid2  43466  nadd2rabex  43484  iscard5  43634  frege124d  43859  mnringmulrcld  44326  climinf  45711  2ffzoeq  47432  iccpartlt  47529  lighneallem2  47711  bgoldbtbndlem3  47912  bgoldbtbndlem4  47913  tgoldbach  47922  fllog2  48674  dignn0ldlem  48708