Theorem mpand 694

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

Syntax hints:   → wi 4   ∧ wa 397

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 206  df-an 398

This theorem is referenced by:  mpani  695  mp2and  698  ecase2dOLD  1030  disjss3  5147  sotri2  6128  fpropnf1  7263  ovig  7551  orduniorsuc  7815  omopth2  8581  onomeneq  9225  frfi  9285  ordunifi  9290  finsschain  9356  cantnfp1lem3  9672  cantnfp1  9673  p1le  12056  nnge1  12237  zltp1le  12609  gtndiv  12636  uzss  12842  eluzaddOLD  12854  uzm1  12857  addlelt  13085  xrre2  13146  xrre3  13147  xrmaxlt  13157  xrmaxle  13159  xrsupsslem  13283  xrub  13288  supxrunb1  13295  zltaddlt1le  13479  nn0p1elfzo  13672  elfzoext  13686  flflp1  13769  ceile  13811  modfzo0difsn  13905  seqf1olem1  14004  leexp2r  14136  expnlbnd2  14194  facavg  14258  wrdred1hash  14508  ccat2s1fvw  14585  caubnd2  15301  limsupbnd1  15423  limsupbnd2  15424  rlim2lt  15438  rlim3  15439  o1co  15527  mulcn2  15537  cn1lem  15539  rlimo1  15558  climsqz  15582  climsqz2  15583  rlimsqzlem  15592  lo1le  15595  rlimno1  15597  climsup  15613  caucvgrlem2  15618  iseraltlem2  15626  iseralt  15628  fsumabs  15744  cvgcmp  15759  cvgcmpce  15761  isumltss  15791  cvgrat  15826  ruclem9  16178  ruclem12  16181  bitsfzolem  16372  bitsfzo  16373  sadcaddlem  16395  gcdzeq  16491  algcvgblem  16511  algcvga  16513  lcmdvdsb  16547  lcmftp  16570  coprm  16645  eulerthlem2  16712  pclem  16768  infpn2  16843  prmreclem1  16846  prmreclem4  16849  ramtlecl  16930  prmgaplem7  16987  initoeu2  17963  lubval  18306  lublecllem  18310  glbval  18319  joinle  18336  latmlem1  18419  odmulg  19419  efginvrel2  19590  pgpfac1lem5  19944  chfacfscmul0  22352  chfacfpmmul0  22356  1stccnp  22958  qustgplem  23617  imasdsf1olem  23871  bldisj  23896  xbln0  23912  prdsbl  23992  metss2lem  24012  stdbdxmet  24016  ngptgp  24137  nghmcn  24254  icoopnst  24447  iocopnst  24448  cnllycmp  24464  iscau3  24787  cmetcaulem  24797  iscmet3lem1  24800  bcthlem4  24836  ovollb2lem  24997  ovolicc2lem3  25028  voliunlem3  25061  volcn  25115  itg10a  25220  itg1ge0a  25221  bddiblnc  25351  dvcnvrelem1  25526  dvfsumrlim  25540  itgsubst  25558  ulmcn  25903  ulmdvlem3  25906  mtest  25908  tanord  26039  emcllem6  26495  ftalem2  26568  chtub  26705  fsumvma2  26707  vmasum  26709  chpchtsum  26712  bcmono  26770  bclbnd  26773  bposlem1  26777  bposlem5  26781  bposlem6  26782  lgsne0  26828  gausslemma2dlem1a  26858  chtppilim  26968  dchrisumlem3  26984  pntrsumbnd2  27060  pntlemf  27098  pntlem3  27102  pntleml  27104  nosupno  27196  noinfno  27211  mulsproplem6  27567  mulsproplem7  27568  upgr2pthnlp  28979  crctcshwlkn0lem3  29056  crctcshwlkn0lem5  29058  eupth2lems  29481  grpoidinvlem3  29747  grpoideu  29750  vacn  29935  blocni  30046  ubthlem2  30112  chscllem2  30879  lnconi  31274  pjnmopi  31389  atomli  31623  sumdmdlem2  31660  cdj3lem2b  31678  xraddge02  31957  fedgmullem1  32703  dfon2lem5  34748  dfon2lem6  34749  cgrcoml  34957  btwnconn2  35063  fvineqsneq  36282  pibt2  36287  ltflcei  36465  poimirlem2  36479  poimirlem18  36495  poimirlem22  36499  poimirlem23  36500  poimirlem26  36503  poimirlem29  36506  poimirlem30  36507  poimirlem32  36509  heicant  36512  mblfinlem3  36516  mblfinlem4  36517  itg2addnclem  36528  itg2addnc  36531  ftc1anclem6  36555  ftc1anc  36558  mettrifi  36614  geomcau  36616  equivbnd  36647  heibor1lem  36666  bfplem1  36679  bfplem2  36680  rrncmslem  36689  divrngidl  36885  lecmtN  38115  cvrletrN  38132  llnnleat  38373  lplnnle2at  38401  lvolnle3at  38442  dalem21  38554  cdlemblem  38653  osumcllem11N  38826  pexmidlem8N  38837  lhpmcvr4N  38886  cdleme32b  39302  cdleme35fnpq  39309  cdleme48bw  39362  cdlemf1  39421  cdlemg2fv2  39460  cdlemg7fvbwN  39467  cdlemg27b  39556  tendoeq2  39634  dia2dimlem1  39924  dihord6apre  40116  dihord5apre  40122  dihglbcpreN  40160  dochnel2  40252  dihjat1lem  40288  dochexmidlem8  40327  mapdordlem2  40497  eqresfnbd  41052  3cubeslem1  41408  ordnexbtwnsuc  42003  naddcnfid2  42104  nadd2rabex  42122  iscard5  42273  frege124d  42498  mnringmulrcld  42973  climinf  44309  2ffzoeq  46023  iccpartlt  46079  lighneallem2  46261  bgoldbtbndlem3  46462  bgoldbtbndlem4  46463  tgoldbach  46472  fllog2  47208  dignn0ldlem  47242