Theorem mp2and 699

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 695	. 2 ⊢ (𝜑 → (𝜒 → 𝜃))
5	1, 4	mpd 15	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:  reu2eqd  3690  ssnelpssd  4064  sotrd  5553  frpomin  6293  fvf1pr  7247  tfisi  7795  tfindsg2  7798  mposn  8039  frxp2  8080  smoord  8291  oelimcl  8521  oeeui  8523  nnawordex  8558  omabs  8572  naddssim  8606  naddel12  8621  ertrd  8644  en2prd  8975  omxpenlem  8997  fodomfir  9218  ixpfi2  9240  supssd  9353  infssd  9384  oismo  9432  cantnflem1c  9583  cantnflem1  9585  cantnflem3  9587  infxpenc2  9919  isfin2-2  10216  axdc2lem  10345  r1limwun  10633  letrd  11276  lelttrd  11277  ltletrd  11279  lttrd  11280  le2subd  11743  ltleaddd  11744  leltaddd  11745  lt2subd  11747  ltmul12a  11983  lemul12ad  12070  lemul12bd  12071  lt2halvesd  12375  uzind  12571  uztrn  12756  xrlttrd  13064  xrlelttrd  13065  xrltletrd  13066  xrletrd  13067  supxrunb1  13224  supxrunb2  13225  ixxun  13267  ixxss1  13269  ixxss2  13270  ixxss12  13271  fldiv4p1lem1div2  13745  fldiv4lem1div2uz2  13746  seqf1o  13956  faclbnd3  14205  relexpindlem  14976  01sqrexlem1  15155  01sqrexlem4  15158  01sqrexlem7  15161  abs3lemd  15377  rlimcn3  15503  o1of2  15526  lo1add  15540  lo1mul  15541  modfsummod  15707  mertenslem1  15797  sin01gt0  16105  cos01gt0  16106  sin02gt0  16107  dvds2addd  16209  dvds2subd  16210  dvdstrd  16212  bezoutlem4  16459  mulgcd  16465  lcmgcdeq  16529  mulgcddvds  16572  rpmulgcd2  16573  rpdvds  16577  divgcdcoprmex  16583  phimullem  16696  eulerthlem1  16698  eulerthlem2  16699  prmdiveq  16703  pythagtriplem4  16737  pcqmul  16771  pcgcd1  16795  pcadd  16807  pockthlem  16823  prmreclem2  16835  4sqlem16  16878  ramub1lem1  16944  ramub1lem2  16945  prmgaplem7  16975  iscatd2  17593  cicsym  17717  initoeu2  17929  joinval  18287  meetval  18301  lattrd  18358  latledi  18389  mulgass  19030  gaorber  19226  psgnunilem4  19415  efgredlem  19665  odadd2  19767  dmdprdpr  19969  ablfacrp2  19987  ablfac1b  19990  ablfac1eu  19993  pgpfac1  20000  orngmul  20786  gsumbagdiaglem  21873  mdetunilem1  22533  mdetunilem4  22536  mdetunilem9  22541  neiptoptop  23052  lmcnp  23225  txcls  23525  txlly  23557  txnlly  23558  tx1stc  23571  alexsubALTlem1  23968  prdsmet  24291  blin2  24350  blcvx  24719  tgqioo  24721  metnrmlem3  24783  iscmet3lem2  25225  ovolmge0  25411  ovolunlem2  25432  mbfi1flimlem  25656  mbfmullem  25659  itg2add  25693  dvferm1lem  25921  dvferm2lem  25923  dvlip2  25933  dvge0  25944  dvcvx  25958  dvfsumabs  25962  ftc1a  25977  plyadd  26155  plymul  26156  dgrlb  26174  plydivlem4  26237  vieta1lem2  26252  ulmdvlem3  26344  sinq12gt0  26449  logdivlti  26562  fsumharmonic  26955  mpodvdsmulf1o  27137  dvdsmulf1o  27139  logfacubnd  27165  perfectlem1  27173  dchrptlem2  27209  2sqlem5  27366  2sqlem8  27370  2sqmod  27380  dchrisum0flblem2  27453  pntibndlem2  27535  pntlemr  27546  pntlemp  27554  nosupbnd1  27659  nosupbnd2lem1  27660  nosupbnd2  27661  noinfbnd1  27674  noinfbnd2lem1  27675  noinfbnd2  27676  noetasuplem4  27681  noetainflem4  27685  slttrd  27704  sltletrd  27705  slelttrd  27706  sletrd  27707  oldbdayim  27840  mulsproplem5  28065  mulsproplem6  28066  mulsproplem7  28067  mulsproplem8  28068  sltmuld  28082  axtgpasch  28451  tgjustr  28458  wlkcompim  29617  wwlksnredwwlkn  29880  wwlksnextsurj  29885  upgr4cycl4dv4e  30172  ex-natded5.2-2  30392  chscllem2  31625  chscllem4  31627  nmopge0  31898  nmfnge0  31914  nmoptrii  32081  staddi  32233  stadd3i  32235  atcvatlem  32372  xrofsup  32757  xrge0addgt0  33005  archiabllem2c  33171  linds2eq  33353  ssdifidlprm  33430  lbsdiflsp0  33646  fedgmullem2  33650  esumpmono  34099  unelldsys  34178  omssubaddlem  34319  signstfvneq0  34592  axtgupdim2ALTV  34688  bnj1098  34802  bnj1110  35001  bnj1121  35004  0nn0m1nnn0  35164  cplgredgex  35172  erdszelem8  35249  txsconn  35292  cvmlift2lem10  35363  cvmlift3lem7  35376  dfon2lem6  35837  dfon2lem8  35839  cgrtr4d  36036  cgrtrand  36044  cgrtr3and  36046  cgrextendand  36060  btwnexch3and  36072  btwnexchand  36077  linecgrand  36133  endofsegidand  36137  btwnconn1lem4  36141  btwnconn1lem8  36145  btwnconn1lem11  36148  btwnconn1lem12  36149  brsegle2  36160  seglecgr12im  36161  segleantisym  36166  colinbtwnle  36169  broutsideof2  36173  outsideoftr  36180  outsidele  36183  lineelsb2  36199  linethru  36204  gtinf  36370  weiunpo  36516  copsex2d  37190  relowlssretop  37414  pibt2  37468  heicant  37701  mbfresfi  37712  ftc1anclem6  37744  eqvreltrd  38710  riotasv2d  39062  lcvnbtwn2  39132  lcvnbtwn3  39133  lcvexchlem4  39142  omlfh1N  39363  atlen0  39415  atlatmstc  39424  cvratlem  39526  lnnat  39532  2atlt  39544  athgt  39561  1cvratex  39578  ps-2  39583  llncmp  39627  llncvrlpln  39663  lplncmp  39667  lplncvrlvol  39721  lvolcmp  39722  dalemcea  39765  dalem-cly  39776  dalem10  39778  dalem17  39785  dalem25  39803  dalem38  39815  dalem44  39821  dalem55  39832  2atm2atN  39890  cdlema1N  39896  paddasslem5  39929  dalawlem3  39978  dalawlem7  39982  dalawlem11  39986  dalawlem12  39987  lhp0lt  40108  4atexlemc  40174  cdlemg33a  40811  cdlemg33  40816  cdlemk51  41058  dia2dimlem2  41170  dia2dimlem3  41171  dihmeetlem20N  41431  coprmdvds2d  42100  flt4lem2  42746  flt4lem5f  42756  ismrcd2  42797  pellqrex  42977  jm2.17b  43059  jm2.26lem3  43099  fnwe2lem2  43149  omabs2  43430  addrcom  44572  infxrunb2  45471  0ellimcdiv  45752  dvnprodlem1  46049  stoweidlem15  46118  stoweidlem26  46129  stoweidlem28  46131  stoweidlem32  46135  stoweidlem44  46147  meadjuni  46560  natglobalincr  46980  dfatcolem  47360  icceuelpart  47541  perfectALTVlem1  47826  bgoldbtbndlem2  47911  bgoldbtbndlem3  47912  copisnmnd  48274  assintopass  48319  lcoss  48542  islindeps2  48589  isldepslvec2  48591  isisod  49133  euendfunc  49632