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  7216  ovig  7507  orduniorsuc  7775  resf1ext2b  7880  omopth2  8514  onomeneq  9143  frfi  9190  ordunifi  9195  finsschain  9264  cantnfp1lem3  9594  cantnfp1  9595  p1le  11991  nnge1  12178  zltp1le  12546  gtndiv  12574  uzss  12779  uzm1  12790  addlelt  13026  xrre2  13090  xrre3  13091  xrmaxlt  13101  xrmaxle  13103  xrsupsslem  13227  xrub  13232  supxrunb1  13239  zltaddlt1le  13426  nn0p1elfzo  13623  flflp1  13732  ceile  13774  modfzo0difsn  13871  seqf1olem1  13969  leexp2r  14102  expnlbnd2  14162  facavg  14229  wrdred1hash  14489  ccat2s1fvw  14567  caubnd2  15286  limsupbnd1  15410  limsupbnd2  15411  rlim2lt  15425  rlim3  15426  o1co  15514  mulcn2  15524  cn1lem  15526  rlimo1  15545  climsqz  15569  climsqz2  15570  rlimsqzlem  15577  lo1le  15580  rlimno1  15582  climsup  15598  caucvgrlem2  15603  iseraltlem2  15611  iseralt  15613  fsumabs  15729  cvgcmp  15744  cvgcmpce  15746  isumltss  15776  cvgrat  15811  ruclem9  16168  ruclem12  16171  bitsfzolem  16366  bitsfzo  16367  sadcaddlem  16389  gcdzeq  16484  algcvgblem  16509  algcvga  16511  lcmdvdsb  16545  lcmftp  16568  coprm  16643  eulerthlem2  16714  pclem  16771  infpn2  16846  prmreclem1  16849  prmreclem4  16852  ramtlecl  16933  prmgaplem7  16990  initoeu2  17945  lubval  18282  lublecllem  18286  glbval  18295  joinle  18312  latmlem1  18397  odmulg  19490  efginvrel2  19661  pgpfac1lem5  20015  chfacfscmul0  22807  chfacfpmmul0  22811  1stccnp  23411  qustgplem  24070  imasdsf1olem  24322  bldisj  24347  xbln0  24363  prdsbl  24440  metss2lem  24460  stdbdxmet  24464  ngptgp  24585  nghmcn  24694  icoopnst  24897  iocopnst  24898  cnllycmp  24916  iscau3  25239  cmetcaulem  25249  iscmet3lem1  25252  bcthlem4  25288  ovollb2lem  25450  ovolicc2lem3  25481  voliunlem3  25514  volcn  25568  itg10a  25672  itg1ge0a  25673  bddiblnc  25804  dvcnvrelem1  25983  dvfsumrlim  25999  itgsubst  26017  ulmcn  26369  ulmdvlem3  26372  mtest  26374  tanord  26508  emcllem6  26972  ftalem2  27045  chtub  27184  fsumvma2  27186  vmasum  27188  chpchtsum  27191  bcmono  27249  bclbnd  27252  bposlem1  27256  bposlem5  27260  bposlem6  27261  lgsne0  27307  gausslemma2dlem1a  27337  chtppilim  27447  dchrisumlem3  27463  pntrsumbnd2  27539  pntlemf  27577  pntlem3  27581  pntleml  27583  nosupno  27676  noinfno  27691  mulsproplem6  28122  mulsproplem7  28123  upgr2pthnlp  29810  crctcshwlkn0lem3  29890  crctcshwlkn0lem5  29892  eupth2lems  30318  grpoidinvlem3  30586  grpoideu  30589  vacn  30774  blocni  30885  ubthlem2  30951  chscllem2  31718  lnconi  32113  pjnmopi  32228  atomli  32462  sumdmdlem2  32499  cdj3lem2b  32517  xraddge02  32840  fedgmullem1  33799  dfon2lem5  35992  dfon2lem6  35993  cgrcoml  36203  btwnconn2  36309  fvineqsneq  37630  pibt2  37635  ltflcei  37822  poimirlem2  37836  poimirlem18  37852  poimirlem22  37856  poimirlem23  37857  poimirlem26  37860  poimirlem29  37863  poimirlem30  37864  poimirlem32  37866  heicant  37869  mblfinlem3  37873  mblfinlem4  37874  itg2addnclem  37885  itg2addnc  37888  ftc1anclem6  37912  ftc1anc  37915  mettrifi  37971  geomcau  37973  equivbnd  38004  heibor1lem  38023  bfplem1  38036  bfplem2  38037  rrncmslem  38046  divrngidl  38242  preuniqval  38710  lecmtN  39595  cvrletrN  39612  llnnleat  39852  lplnnle2at  39880  lvolnle3at  39921  dalem21  40033  cdlemblem  40132  osumcllem11N  40305  pexmidlem8N  40316  lhpmcvr4N  40365  cdleme32b  40781  cdleme35fnpq  40788  cdleme48bw  40841  cdlemf1  40900  cdlemg2fv2  40939  cdlemg7fvbwN  40946  cdlemg27b  41035  tendoeq2  41113  dia2dimlem1  41403  dihord6apre  41595  dihord5apre  41601  dihglbcpreN  41639  dochnel2  41731  dihjat1lem  41767  dochexmidlem8  41806  mapdordlem2  41976  eqresfnbd  42567  3cubeslem1  43004  ordnexbtwnsuc  43587  naddcnfid2  43688  nadd2rabex  43706  iscard5  43855  frege124d  44080  mnringmulrcld  44547  climinf  45929  2ffzoeq  47650  iccpartlt  47747  lighneallem2  47929  bgoldbtbndlem3  48130  bgoldbtbndlem4  48131  tgoldbach  48140  fllog2  48891  dignn0ldlem  48925