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  3709  ssnelpssd  4080  sotrd  5574  frpomin  6315  fvf1pr  7284  tfisi  7837  tfindsg2  7840  mposn  8084  frxp2  8125  smoord  8336  oelimcl  8566  oeeui  8568  nnawordex  8603  omabs  8617  naddssim  8651  naddel12  8666  ertrd  8689  en2prd  9021  omxpenlem  9046  fodomfir  9285  ixpfi2  9307  supssd  9420  infssd  9451  oismo  9499  cantnflem1c  9646  cantnflem1  9648  cantnflem3  9650  infxpenc2  9981  isfin2-2  10278  axdc2lem  10407  r1limwun  10695  letrd  11337  lelttrd  11338  ltletrd  11340  lttrd  11341  le2subd  11804  ltleaddd  11805  leltaddd  11806  lt2subd  11808  ltmul12a  12044  lemul12ad  12131  lemul12bd  12132  lt2halvesd  12436  uzind  12632  uztrn  12817  xrlttrd  13125  xrlelttrd  13126  xrltletrd  13127  xrletrd  13128  supxrunb1  13285  supxrunb2  13286  ixxun  13328  ixxss1  13330  ixxss2  13331  ixxss12  13332  fldiv4p1lem1div2  13803  fldiv4lem1div2uz2  13804  seqf1o  14014  faclbnd3  14263  relexpindlem  15035  01sqrexlem1  15214  01sqrexlem4  15217  01sqrexlem7  15220  abs3lemd  15436  rlimcn3  15562  o1of2  15585  lo1add  15599  lo1mul  15600  modfsummod  15766  mertenslem1  15856  sin01gt0  16164  cos01gt0  16165  sin02gt0  16166  dvds2addd  16268  dvds2subd  16269  dvdstrd  16271  bezoutlem4  16518  mulgcd  16524  lcmgcdeq  16588  mulgcddvds  16631  rpmulgcd2  16632  rpdvds  16636  divgcdcoprmex  16642  phimullem  16755  eulerthlem1  16757  eulerthlem2  16758  prmdiveq  16762  pythagtriplem4  16796  pcqmul  16830  pcgcd1  16854  pcadd  16866  pockthlem  16882  prmreclem2  16894  4sqlem16  16937  ramub1lem1  17003  ramub1lem2  17004  prmgaplem7  17034  iscatd2  17648  cicsym  17772  initoeu2  17984  joinval  18342  meetval  18356  lattrd  18411  latledi  18442  mulgass  19049  gaorber  19246  psgnunilem4  19433  efgredlem  19683  odadd2  19785  dmdprdpr  19987  ablfacrp2  20005  ablfac1b  20008  ablfac1eu  20011  pgpfac1  20018  gsumbagdiaglem  21845  mdetunilem1  22505  mdetunilem4  22508  mdetunilem9  22513  neiptoptop  23024  lmcnp  23197  txcls  23497  txlly  23529  txnlly  23530  tx1stc  23543  alexsubALTlem1  23940  prdsmet  24264  blin2  24323  blcvx  24692  tgqioo  24694  metnrmlem3  24756  iscmet3lem2  25198  ovolmge0  25384  ovolunlem2  25405  mbfi1flimlem  25629  mbfmullem  25632  itg2add  25666  dvferm1lem  25894  dvferm2lem  25896  dvlip2  25906  dvge0  25917  dvcvx  25931  dvfsumabs  25935  ftc1a  25950  plyadd  26128  plymul  26129  dgrlb  26147  plydivlem4  26210  vieta1lem2  26225  ulmdvlem3  26317  sinq12gt0  26422  logdivlti  26535  fsumharmonic  26928  mpodvdsmulf1o  27110  dvdsmulf1o  27112  logfacubnd  27138  perfectlem1  27146  dchrptlem2  27182  2sqlem5  27339  2sqlem8  27343  2sqmod  27353  dchrisum0flblem2  27426  pntibndlem2  27508  pntlemr  27519  pntlemp  27527  nosupbnd1  27632  nosupbnd2lem1  27633  nosupbnd2  27634  noinfbnd1  27647  noinfbnd2lem1  27648  noinfbnd2  27649  noetasuplem4  27654  noetainflem4  27658  slttrd  27677  sltletrd  27678  slelttrd  27679  sletrd  27680  oldbdayim  27806  mulsproplem5  28029  mulsproplem6  28030  mulsproplem7  28031  mulsproplem8  28032  sltmuld  28046  axtgpasch  28400  tgjustr  28407  wlkcompim  29566  wwlksnredwwlkn  29831  wwlksnextsurj  29836  upgr4cycl4dv4e  30120  ex-natded5.2-2  30340  chscllem2  31573  chscllem4  31575  nmopge0  31846  nmfnge0  31862  nmoptrii  32029  staddi  32181  stadd3i  32183  atcvatlem  32320  xrofsup  32696  xrge0addgt0  32964  archiabllem2c  33155  orngmul  33287  linds2eq  33358  ssdifidlprm  33435  lbsdiflsp0  33628  fedgmullem2  33632  esumpmono  34075  unelldsys  34154  omssubaddlem  34296  signstfvneq0  34569  axtgupdim2ALTV  34665  bnj1098  34779  bnj1110  34978  bnj1121  34981  0nn0m1nnn0  35100  cplgredgex  35108  erdszelem8  35185  txsconn  35228  cvmlift2lem10  35299  cvmlift3lem7  35312  dfon2lem6  35771  dfon2lem8  35773  cgrtr4d  35968  cgrtrand  35976  cgrtr3and  35978  cgrextendand  35992  btwnexch3and  36004  btwnexchand  36009  linecgrand  36065  endofsegidand  36069  btwnconn1lem4  36073  btwnconn1lem8  36077  btwnconn1lem11  36080  btwnconn1lem12  36081  brsegle2  36092  seglecgr12im  36093  segleantisym  36098  colinbtwnle  36101  broutsideof2  36105  outsideoftr  36112  outsidele  36115  lineelsb2  36131  linethru  36136  gtinf  36302  weiunpo  36448  copsex2d  37122  relowlssretop  37346  pibt2  37400  heicant  37644  mbfresfi  37655  ftc1anclem6  37687  eqvreltrd  38594  riotasv2d  38945  lcvnbtwn2  39015  lcvnbtwn3  39016  lcvexchlem4  39025  omlfh1N  39246  atlen0  39298  atlatmstc  39307  cvratlem  39410  lnnat  39416  2atlt  39428  athgt  39445  1cvratex  39462  ps-2  39467  llncmp  39511  llncvrlpln  39547  lplncmp  39551  lplncvrlvol  39605  lvolcmp  39606  dalemcea  39649  dalem-cly  39660  dalem10  39662  dalem17  39669  dalem25  39687  dalem38  39699  dalem44  39705  dalem55  39716  2atm2atN  39774  cdlema1N  39780  paddasslem5  39813  dalawlem3  39862  dalawlem7  39866  dalawlem11  39870  dalawlem12  39871  lhp0lt  39992  4atexlemc  40058  cdlemg33a  40695  cdlemg33  40700  cdlemk51  40942  dia2dimlem2  41054  dia2dimlem3  41055  dihmeetlem20N  41315  coprmdvds2d  41984  flt4lem2  42628  flt4lem5f  42638  ismrcd2  42680  pellqrex  42860  jm2.17b  42943  jm2.26lem3  42983  fnwe2lem2  43033  omabs2  43314  addrcom  44457  infxrunb2  45357  0ellimcdiv  45640  dvnprodlem1  45937  stoweidlem15  46006  stoweidlem26  46017  stoweidlem28  46019  stoweidlem32  46023  stoweidlem44  46035  meadjuni  46448  natglobalincr  46868  dfatcolem  47246  icceuelpart  47427  perfectALTVlem1  47712  bgoldbtbndlem2  47797  bgoldbtbndlem3  47798  copisnmnd  48147  assintopass  48192  lcoss  48415  islindeps2  48462  isldepslvec2  48464  isisod  49006  euendfunc  49505