Theorem mpand 708

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 471	. 2 ⊢ (𝜑 → ((𝜒 ∧ 𝜓) → 𝜃))
4	1, 3	mpan2d 707	1 ⊢ (𝜑 → (𝜒 → 𝜃))

This proof depends on syntax axioms:   → wi 4   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  mpani  709  mp2and  712  disjss3  5106  sotri2  6127  fpropnf1  7267  ovig  7562  orduniorsuc  7829  resf1ext2b  7935  omopth2  8574  onomeneq  9211  frfi  9258  ordunifi  9263  finsschain  9329  cantnfp1lem3  9662  cantnfp1  9663  p1le  12087  nnge1  12291  zltp1le  12671  gtndiv  12701  uzss  12913  uzm1  12924  addlelt  13160  xrre2  13224  xrre3  13225  xrmaxlt  13235  xrmaxle  13237  xrsupsslem  13361  xrub  13366  supxrunb1  13373  zltaddlt1le  13560  nn0p1elfzo  13760  flflp1  13870  ceile  13912  modfzo0difsn  14009  seqf1olem1  14107  leexp2r  14240  expnlbnd2  14300  facavg  14367  wrdred1hash  14628  ccat2s1fvw  14708  caubnd2  15447  limsupbnd1  15571  limsupbnd2  15572  rlim2lt  15586  rlim3  15587  o1co  15675  mulcn2  15685  cn1lem  15687  rlimo1  15706  climsqz  15730  climsqz2  15731  rlimsqzlem  15738  lo1le  15741  rlimno1  15743  climsup  15759  caucvgrlem2  15764  iseraltlem2  15772  iseralt  15774  fsumabs  15890  cvgcmp  15905  cvgcmpce  15907  isumltss  15939  cvgrat  15974  ruclem9  16330  ruclem12  16333  bitsfzolem  16528  bitsfzo  16529  sadcaddlem  16551  gcdzeq  16646  algcvgblem  16671  algcvga  16673  lcmdvdsb  16707  lcmftp  16730  coprm  16806  eulerthlem2  16877  pclem  16934  infpn2  17009  prmreclem1  17012  prmreclem4  17015  ramtlecl  17096  prmgaplem7  17153  initoeu2  18109  lubval  18446  lublecllem  18450  glbval  18459  joinle  18476  latmlem1  18561  odmulg  19684  efginvrel2  19855  pgpfac1lem5  20209  chfacfscmul0  23084  chfacfpmmul0  23088  1stccnp  23689  qustgplem  24348  imasdsf1olem  24600  bldisj  24625  xbln0  24641  prdsbl  24718  metss2lem  24738  stdbdxmet  24742  ngptgp  24863  nghmcn  24972  icoopnst  25168  iocopnst  25169  cnllycmp  25185  iscau3  25507  cmetcaulem  25517  iscmet3lem1  25520  bcthlem4  25556  ovollb2lem  25717  ovolicc2lem3  25748  voliunlem3  25781  volcn  25835  itg10a  25939  itg1ge0a  25940  bddiblnc  26071  dvcnvrelem1  26246  dvfsumrlim  26260  itgsubst  26278  ulmcn  26632  ulmdvlem3  26635  mtest  26637  tanord  26773  emcllem6  27235  ftalem2  27308  chtub  27446  fsumvma2  27448  vmasum  27450  chpchtsum  27453  bcmono  27511  bclbnd  27514  bposlem1  27518  bposlem5  27522  bposlem6  27523  lgsne0  27569  gausslemma2dlem1a  27599  chtppilim  27709  dchrisumlem3  27725  pntrsumbnd2  27801  pntlemf  27839  pntlem3  27843  pntleml  27845  nosupno  27937  noinfno  27952  mulsproplem6  28384  mulsproplem7  28385  upgr2pthnlp  30183  crctcshwlkn0lem3  30266  crctcshwlkn0lem5  30268  eupth2lems  30704  grpoidinvlem3  30973  grpoideu  30976  vacn  31161  blocni  31272  ubthlem2  31338  chscllem2  32105  lnconi  32500  pjnmopi  32615  atomli  32849  sumdmdlem2  32886  cdj3lem2b  32904  xraddge02  33215  fedgmullem1  34126  dfon2lem5  36351  dfon2lem6  36352  cgrcoml  36563  btwnconn2  36669  fvineqsneq  38153  pibt2  38158  ltflcei  38349  poimirlem2  38358  poimirlem18  38374  poimirlem22  38378  poimirlem23  38379  poimirlem26  38382  poimirlem29  38385  poimirlem30  38386  poimirlem32  38388  heicant  38391  mblfinlem3  38395  mblfinlem4  38396  itg2addnclem  38407  itg2addnc  38410  ftc1anclem6  38434  ftc1anc  38437  mettrifi  38494  geomcau  38496  equivbnd  38527  heibor1lem  38546  bfplem1  38559  bfplem2  38560  rrncmslem  38569  divrngidl  38765  preuniqval  39231  lecmtN  40116  cvrletrN  40133  llnnleat  40373  lplnnle2at  40401  lvolnle3at  40442  dalem21  40554  cdlemblem  40653  osumcllem11N  40826  pexmidlem8N  40837  lhpmcvr4N  40886  cdleme32b  41302  cdleme35fnpq  41309  cdleme48bw  41362  cdlemf1  41421  cdlemg2fv2  41460  cdlemg7fvbwN  41467  cdlemg27b  41556  tendoeq2  41634  dia2dimlem1  41924  dihord6apre  42116  dihord5apre  42122  dihglbcpreN  42160  dochnel2  42252  dihjat1lem  42288  dochexmidlem8  42327  mapdordlem2  42497  eqresfnbd  43089  3cubeslem1  43516  ordnexbtwnsuc  44095  naddcnfid2  44196  nadd2rabex  44214  iscard5  44363  frege124d  44588  mnringmulrcld  45053  climinf  46423  2ffzoeq  48203  iccpartlt  48311  lighneallem2  48496  bgoldbtbndlem3  48710  bgoldbtbndlem4  48711  tgoldbach  48720  fllog2  49485  dignn0ldlem  49519