Theorem mpand 696

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 695	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  697  mp2and  700  disjss3  5098  sotri2  6087  fpropnf1  7215  ovig  7506  orduniorsuc  7774  resf1ext2b  7879  omopth2  8513  onomeneq  9142  frfi  9189  ordunifi  9194  finsschain  9263  cantnfp1lem3  9593  cantnfp1  9594  p1le  11990  nnge1  12177  zltp1le  12545  gtndiv  12573  uzss  12778  uzm1  12789  addlelt  13025  xrre2  13089  xrre3  13090  xrmaxlt  13100  xrmaxle  13102  xrsupsslem  13226  xrub  13231  supxrunb1  13238  zltaddlt1le  13425  nn0p1elfzo  13622  flflp1  13731  ceile  13773  modfzo0difsn  13870  seqf1olem1  13968  leexp2r  14101  expnlbnd2  14161  facavg  14228  wrdred1hash  14488  ccat2s1fvw  14566  caubnd2  15285  limsupbnd1  15409  limsupbnd2  15410  rlim2lt  15424  rlim3  15425  o1co  15513  mulcn2  15523  cn1lem  15525  rlimo1  15544  climsqz  15568  climsqz2  15569  rlimsqzlem  15576  lo1le  15579  rlimno1  15581  climsup  15597  caucvgrlem2  15602  iseraltlem2  15610  iseralt  15612  fsumabs  15728  cvgcmp  15743  cvgcmpce  15745  isumltss  15775  cvgrat  15810  ruclem9  16167  ruclem12  16170  bitsfzolem  16365  bitsfzo  16366  sadcaddlem  16388  gcdzeq  16483  algcvgblem  16508  algcvga  16510  lcmdvdsb  16544  lcmftp  16567  coprm  16642  eulerthlem2  16713  pclem  16770  infpn2  16845  prmreclem1  16848  prmreclem4  16851  ramtlecl  16932  prmgaplem7  16989  initoeu2  17944  lubval  18281  lublecllem  18285  glbval  18294  joinle  18311  latmlem1  18396  odmulg  19489  efginvrel2  19660  pgpfac1lem5  20014  chfacfscmul0  22806  chfacfpmmul0  22810  1stccnp  23410  qustgplem  24069  imasdsf1olem  24321  bldisj  24346  xbln0  24362  prdsbl  24439  metss2lem  24459  stdbdxmet  24463  ngptgp  24584  nghmcn  24693  icoopnst  24896  iocopnst  24897  cnllycmp  24915  iscau3  25238  cmetcaulem  25248  iscmet3lem1  25251  bcthlem4  25287  ovollb2lem  25449  ovolicc2lem3  25480  voliunlem3  25513  volcn  25567  itg10a  25671  itg1ge0a  25672  bddiblnc  25803  dvcnvrelem1  25982  dvfsumrlim  25998  itgsubst  26016  ulmcn  26368  ulmdvlem3  26371  mtest  26373  tanord  26507  emcllem6  26971  ftalem2  27044  chtub  27183  fsumvma2  27185  vmasum  27187  chpchtsum  27190  bcmono  27248  bclbnd  27251  bposlem1  27255  bposlem5  27259  bposlem6  27260  lgsne0  27306  gausslemma2dlem1a  27336  chtppilim  27446  dchrisumlem3  27462  pntrsumbnd2  27538  pntlemf  27576  pntlem3  27580  pntleml  27582  nosupno  27675  noinfno  27690  mulsproplem6  28103  mulsproplem7  28104  bdayfinbndlem1  28446  upgr2pthnlp  29788  crctcshwlkn0lem3  29868  crctcshwlkn0lem5  29870  eupth2lems  30296  grpoidinvlem3  30564  grpoideu  30567  vacn  30752  blocni  30863  ubthlem2  30929  chscllem2  31696  lnconi  32091  pjnmopi  32206  atomli  32440  sumdmdlem2  32477  cdj3lem2b  32495  xraddge02  32818  fedgmullem1  33767  dfon2lem5  35960  dfon2lem6  35961  cgrcoml  36171  btwnconn2  36277  fvineqsneq  37588  pibt2  37593  ltflcei  37780  poimirlem2  37794  poimirlem18  37810  poimirlem22  37814  poimirlem23  37815  poimirlem26  37818  poimirlem29  37821  poimirlem30  37822  poimirlem32  37824  heicant  37827  mblfinlem3  37831  mblfinlem4  37832  itg2addnclem  37843  itg2addnc  37846  ftc1anclem6  37870  ftc1anc  37873  mettrifi  37929  geomcau  37931  equivbnd  37962  heibor1lem  37981  bfplem1  37994  bfplem2  37995  rrncmslem  38004  divrngidl  38200  preuniqval  38668  lecmtN  39553  cvrletrN  39570  llnnleat  39810  lplnnle2at  39838  lvolnle3at  39879  dalem21  39991  cdlemblem  40090  osumcllem11N  40263  pexmidlem8N  40274  lhpmcvr4N  40323  cdleme32b  40739  cdleme35fnpq  40746  cdleme48bw  40799  cdlemf1  40858  cdlemg2fv2  40897  cdlemg7fvbwN  40904  cdlemg27b  40993  tendoeq2  41071  dia2dimlem1  41361  dihord6apre  41553  dihord5apre  41559  dihglbcpreN  41597  dochnel2  41689  dihjat1lem  41725  dochexmidlem8  41764  mapdordlem2  41934  eqresfnbd  42525  3cubeslem1  42962  ordnexbtwnsuc  43545  naddcnfid2  43646  nadd2rabex  43664  iscard5  43813  frege124d  44038  mnringmulrcld  44505  climinf  45888  2ffzoeq  47609  iccpartlt  47706  lighneallem2  47888  bgoldbtbndlem3  48089  bgoldbtbndlem4  48090  tgoldbach  48099  fllog2  48850  dignn0ldlem  48884