Theorem mpand 705

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

Syntax hints:   → wi 4   ∧ wa 399

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 209  df-an 400

This theorem is referenced by:  mpani  706  mp2and  709  disjss3  5100  sotri2  6116  fpropnf1  7251  ovig  7542  orduniorsuc  7810  resf1ext2b  7916  omopth2  8553  onomeneq  9182  frfi  9229  ordunifi  9234  finsschain  9300  cantnfp1lem3  9633  cantnfp1  9634  p1le  12047  nnge1  12251  zltp1le  12631  gtndiv  12660  uzss  12872  uzm1  12883  addlelt  13119  xrre2  13183  xrre3  13184  xrmaxlt  13194  xrmaxle  13196  xrsupsslem  13320  xrub  13325  supxrunb1  13332  zltaddlt1le  13519  nn0p1elfzo  13718  flflp1  13827  ceile  13869  modfzo0difsn  13966  seqf1olem1  14064  leexp2r  14197  expnlbnd2  14257  facavg  14324  wrdred1hash  14584  ccat2s1fvw  14662  caubnd2  15395  limsupbnd1  15519  limsupbnd2  15520  rlim2lt  15534  rlim3  15535  o1co  15623  mulcn2  15633  cn1lem  15635  rlimo1  15654  climsqz  15678  climsqz2  15679  rlimsqzlem  15686  lo1le  15689  rlimno1  15691  climsup  15707  caucvgrlem2  15712  iseraltlem2  15720  iseralt  15722  fsumabs  15839  cvgcmp  15854  cvgcmpce  15856  isumltss  15888  cvgrat  15923  ruclem9  16280  ruclem12  16283  bitsfzolem  16478  bitsfzo  16479  sadcaddlem  16501  gcdzeq  16596  algcvgblem  16621  algcvga  16623  lcmdvdsb  16657  lcmftp  16680  coprm  16756  eulerthlem2  16827  pclem  16884  infpn2  16959  prmreclem1  16962  prmreclem4  16965  ramtlecl  17046  prmgaplem7  17103  initoeu2  18059  lubval  18396  lublecllem  18400  glbval  18409  joinle  18426  latmlem1  18511  odmulg  19606  efginvrel2  19777  pgpfac1lem5  20131  chfacfscmul0  22925  chfacfpmmul0  22929  1stccnp  23529  qustgplem  24188  imasdsf1olem  24440  bldisj  24465  xbln0  24481  prdsbl  24558  metss2lem  24578  stdbdxmet  24582  ngptgp  24703  nghmcn  24812  icoopnst  25008  iocopnst  25009  cnllycmp  25025  iscau3  25347  cmetcaulem  25357  iscmet3lem1  25360  bcthlem4  25396  ovollb2lem  25557  ovolicc2lem3  25588  voliunlem3  25621  volcn  25675  itg10a  25779  itg1ge0a  25780  bddiblnc  25911  dvcnvrelem1  26086  dvfsumrlim  26100  itgsubst  26118  ulmcn  26469  ulmdvlem3  26472  mtest  26474  tanord  26610  emcllem6  27072  ftalem2  27145  chtub  27283  fsumvma2  27285  vmasum  27287  chpchtsum  27290  bcmono  27348  bclbnd  27351  bposlem1  27355  bposlem5  27359  bposlem6  27360  lgsne0  27406  gausslemma2dlem1a  27436  chtppilim  27546  dchrisumlem3  27562  pntrsumbnd2  27638  pntlemf  27676  pntlem3  27680  pntleml  27682  nosupno  27774  noinfno  27789  mulsproplem6  28221  mulsproplem7  28222  upgr2pthnlp  29939  crctcshwlkn0lem3  30019  crctcshwlkn0lem5  30021  eupth2lems  30447  grpoidinvlem3  30716  grpoideu  30719  vacn  30904  blocni  31015  ubthlem2  31081  chscllem2  31848  lnconi  32243  pjnmopi  32358  atomli  32592  sumdmdlem2  32629  cdj3lem2b  32647  xraddge02  32965  fedgmullem1  33928  dfon2lem5  36140  dfon2lem6  36141  cgrcoml  36351  btwnconn2  36457  fvineqsneq  37911  pibt2  37916  ltflcei  38112  poimirlem2  38126  poimirlem18  38142  poimirlem22  38146  poimirlem23  38147  poimirlem26  38150  poimirlem29  38153  poimirlem30  38154  poimirlem32  38156  heicant  38159  mblfinlem3  38163  mblfinlem4  38164  itg2addnclem  38175  itg2addnc  38178  ftc1anclem6  38202  ftc1anc  38205  mettrifi  38261  geomcau  38263  equivbnd  38294  heibor1lem  38313  bfplem1  38326  bfplem2  38327  rrncmslem  38336  divrngidl  38532  preuniqval  39000  lecmtN  39885  cvrletrN  39902  llnnleat  40142  lplnnle2at  40170  lvolnle3at  40211  dalem21  40323  cdlemblem  40422  osumcllem11N  40595  pexmidlem8N  40606  lhpmcvr4N  40655  cdleme32b  41071  cdleme35fnpq  41078  cdleme48bw  41131  cdlemf1  41190  cdlemg2fv2  41229  cdlemg7fvbwN  41236  cdlemg27b  41325  tendoeq2  41403  dia2dimlem1  41693  dihord6apre  41885  dihord5apre  41891  dihglbcpreN  41929  dochnel2  42021  dihjat1lem  42057  dochexmidlem8  42096  mapdordlem2  42266  eqresfnbd  42856  3cubeslem1  43270  ordnexbtwnsuc  43849  naddcnfid2  43950  nadd2rabex  43968  iscard5  44117  frege124d  44342  mnringmulrcld  44809  climinf  46173  2ffzoeq  47913  iccpartlt  48021  lighneallem2  48206  bgoldbtbndlem3  48420  bgoldbtbndlem4  48421  tgoldbach  48430  fllog2  49181  dignn0ldlem  49215