Theorem mp2and 711

Description: A deduction based on modus ponens. (Contributed by NM, 12-Dec-2004.)

Hypotheses

Ref	Expression
mp2and.1	⊢ (𝜑 → 𝜓)
mp2and.2	⊢ (𝜑 → 𝜒)
mp2and.3	⊢ (𝜑 → ((𝜓 ∧ 𝜒) → 𝜃))

Assertion

Ref	Expression
mp2and	⊢ (𝜑 → 𝜃)

Proof of Theorem mp2and

Step	Hyp	Ref	Expression
1		mp2and.2	. 2 ⊢ (𝜑 → 𝜒)
2		mp2and.1	. . 3 ⊢ (𝜑 → 𝜓)
3		mp2and.3	. . 3 ⊢ (𝜑 → ((𝜓 ∧ 𝜒) → 𝜃))
4	2, 3	mpand 707	. 2 ⊢ (𝜑 → (𝜒 → 𝜃))
5	1, 4	mpd 16	1 ⊢ (𝜑 → 𝜃)

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

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 401

This theorem is used by:  reu2eqd  3698  ssnelpssd  4069  sotrd  5594  frpomin  6341  fvf1pr  7305  tfisi  7853  tfindsg2  7856  mposn  8096  frxp2  8138  smoord  8350  oelimcl  8584  oeeui  8586  nnawordex  8621  omabs  8635  naddssim  8670  naddel12  8685  ertrd  8709  en2prd  9042  omxpenlem  9064  fodomfir  9285  ixpfi2  9305  supssd  9421  infssd  9452  oismo  9500  cantnflem1c  9654  cantnflem1  9656  cantnflem3  9658  infxpenc2  10013  isfin2-2  10309  axdc2lem  10438  r1limwun  10727  letrd  11373  lelttrd  11374  ltletrd  11376  lttrd  11377  le2subd  11840  ltleaddd  11841  leltaddd  11842  lt2subd  11844  ltmul12a  12077  lemul12ad  12163  lemul12bd  12164  lt2halvesd  12498  uzind  12694  uztrn  12886  xrlttrd  13190  xrlelttrd  13191  xrltletrd  13192  xrletrd  13193  supxrunb1  13351  supxrunb2  13352  ixxun  13394  ixxss1  13396  ixxss2  13397  ixxss12  13398  fldiv4p1lem1div2  13875  fldiv4lem1div2uz2  13876  seqf1o  14086  faclbnd3  14335  relexpindlem  15107  01sqrexlem1  15300  01sqrexlem4  15303  01sqrexlem7  15306  abs3lemd  15522  rlimcn3  15648  o1of2  15671  lo1add  15685  lo1mul  15686  modfsummod  15853  mertenslem1  15945  sin01gt0  16252  cos01gt0  16253  sin02gt0  16254  dvds2addd  16356  dvds2subd  16357  dvdstrd  16359  bezoutlem4  16606  mulgcd  16612  lcmgcdeq  16676  mulgcddvds  16719  rpmulgcd2  16720  rpdvds  16724  divgcdcoprmex  16730  phimullem  16844  eulerthlem1  16846  eulerthlem2  16847  prmdiveq  16851  pythagtriplem4  16885  pcqmul  16919  pcgcd1  16943  pcadd  16955  pockthlem  16971  prmreclem2  16983  4sqlem16  17026  ramub1lem1  17092  ramub1lem2  17093  prmgaplem7  17123  iscatd2  17743  cicsym  17867  initoeu2  18079  joinval  18437  meetval  18451  lattrd  18508  latledi  18539  mulgass  19183  gaorber  19384  psgnunilem4  19573  efgredlem  19823  odadd2  19925  dmdprdpr  20127  ablfacrp2  20145  ablfac1b  20148  ablfac1eu  20151  pgpfac1  20158  orngmul  20979  ssdifidlprm  21497  gsumbagdiaglem  22092  mdetunilem1  22780  mdetunilem4  22783  mdetunilem9  22788  neiptoptop  23299  lmcnp  23472  txcls  23772  txlly  23804  txnlly  23805  tx1stc  23818  alexsubALTlem1  24215  prdsmet  24538  blin2  24597  blcvx  24966  tgqioo  24968  metnrmlem3  25030  iscmet3lem2  25462  ovolmge0  25647  ovolunlem2  25668  mbfi1flimlem  25892  mbfmullem  25895  itg2add  25929  dvferm1lem  26154  dvferm2lem  26156  dvlip2  26165  dvge0  26176  dvcvx  26190  dvfsumabs  26193  ftc1a  26207  plyadd  26385  plymul  26386  dgrlb  26404  plydivlem4  26468  vieta1lem2  26483  ulmdvlem3  26576  sinq12gt0  26683  logdivlti  26796  fsumharmonic  27187  mpodvdsmulf1o  27369  dvdsmulf1o  27371  logfacubnd  27396  perfectlem1  27404  dchrptlem2  27440  2sqlem5  27597  2sqlem8  27601  2sqmod  27611  dchrisum0flblem2  27684  pntibndlem2  27766  pntlemr  27777  pntlemp  27785  nosupbnd1  27889  nosupbnd2lem1  27890  nosupbnd2  27891  noinfbnd1  27904  noinfbnd2lem1  27905  noinfbnd2  27906  noetasuplem4  27911  noetainflem4  27915  ltstrd  27938  ltlestrd  27939  leltstrd  27940  lestrd  27941  oldbdayim  28093  mulsproplem5  28324  mulsproplem6  28325  mulsproplem7  28326  mulsproplem8  28327  ltmulsd  28341  bdayfinbndlem1  28671  bdayfinbnd  28673  axtgpasch  28747  tgjustr  28754  wlkcompim  29992  wwlksnredwwlkn  30255  wwlksnextsurj  30260  upgr4cycl4dv4e  30547  ex-natded5.2-2  30767  chscllem2  32001  chscllem4  32003  nmopge0  32274  nmfnge0  32290  nmoptrii  32457  staddi  32609  stadd3i  32611  atcvatlem  32748  xrofsup  33123  xrge0addgt0  33346  archiabllem2c  33524  linds2eq  33703  lbsdiflsp0  34025  fedgmullem2  34029  esumpmono  34478  unelldsys  34557  omssubaddlem  34698  signstfvneq0  34968  axtgupdim2ALTV  35064  bnj1098  35181  bnj1110  35379  bnj1121  35382  0nn0m1nnn0  35612  cplgredgex  35621  erdszelem8  35698  txsconn  35741  cvmlift2lem10  35812  cvmlift3lem7  35825  dfon2lem6  36286  dfon2lem8  36288  cgrtr4d  36485  cgrtrand  36493  cgrtr3and  36495  cgrextendand  36509  btwnexch3and  36521  btwnexchand  36526  linecgrand  36582  endofsegidand  36586  btwnconn1lem4  36590  btwnconn1lem8  36594  btwnconn1lem11  36597  btwnconn1lem12  36598  brsegle2  36609  seglecgr12im  36610  segleantisym  36615  colinbtwnle  36618  broutsideof2  36622  outsideoftr  36629  outsidele  36632  lineelsb2  36648  linethru  36653  ontr2d  36700  ltnadd  36718  gtinf  36858  weiunpo  37004  copsex2d  37811  relowlssretop  38037  pibt2  38091  heicant  38334  mbfresfi  38345  ftc1anclem6  38377  eqvreltrd  39369  riotasv2d  39759  lcvnbtwn2  39829  lcvnbtwn3  39830  lcvexchlem4  39839  omlfh1N  40060  atlen0  40112  atlatmstc  40121  cvratlem  40223  lnnat  40229  2atlt  40241  athgt  40258  1cvratex  40275  ps-2  40280  llncmp  40324  llncvrlpln  40360  lplncmp  40364  lplncvrlvol  40418  lvolcmp  40419  dalemcea  40462  dalem-cly  40473  dalem10  40475  dalem17  40482  dalem25  40500  dalem38  40512  dalem44  40518  dalem55  40529  2atm2atN  40587  cdlema1N  40593  paddasslem5  40626  dalawlem3  40675  dalawlem7  40679  dalawlem11  40683  dalawlem12  40684  lhp0lt  40805  4atexlemc  40871  cdlemg33a  41508  cdlemg33  41513  cdlemk51  41755  dia2dimlem2  41867  dia2dimlem3  41868  dihmeetlem20N  42128  coprmdvds2d  42796  flt4lem2  43407  flt4lem5f  43417  ismrcd2  43458  pellqrex  43634  jm2.17b  43716  jm2.26lem3  43756  fnwe2lem2  43806  omabs2  44087  addrcom  45211  infxrunb2  46111  0ellimcdiv  46391  dvnprodlem1  46688  stoweidlem15  46757  stoweidlem26  46768  stoweidlem28  46770  stoweidlem32  46774  stoweidlem44  46786  meadjuni  47199  natglobalincr  47621  dfatcolem  48020  icceuelpart  48213  perfectALTVlem1  48514  bgoldbtbndlem2  48599  bgoldbtbndlem3  48600  copisnmnd  48962  assintopass  49007  lcoss  49244  islindeps2  49291  isldepslvec2  49293  isisod  49833  euendfunc  50332