Theorem mp2and 707

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 703	. 2 ⊢ (𝜑 → (𝜒 → 𝜃))
5	1, 4	mpd 15	1 ⊢ (𝜑 → 𝜃)

Syntax hints:   → wi 4   ∧ wa 398

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 209  df-an 399

This theorem is referenced by:  reu2eqd  3689  ssnelpssd  4060  sotrd  5570  frpomin  6312  fvf1pr  7276  tfisi  7824  tfindsg2  7827  mposn  8066  frxp2  8108  smoord  8320  oelimcl  8554  oeeui  8556  nnawordex  8591  omabs  8605  naddssim  8640  naddel12  8655  ertrd  8679  en2prd  9013  omxpenlem  9035  fodomfir  9257  ixpfi2  9279  supssd  9395  infssd  9426  oismo  9474  cantnflem1c  9628  cantnflem1  9630  cantnflem3  9632  infxpenc2  9964  isfin2-2  10262  axdc2lem  10391  r1limwun  10680  letrd  11326  lelttrd  11327  ltletrd  11329  lttrd  11330  le2subd  11793  ltleaddd  11794  leltaddd  11795  lt2subd  11797  ltmul12a  12033  lemul12ad  12120  lemul12bd  12121  lt2halvesd  12455  uzind  12651  uztrn  12843  xrlttrd  13147  xrlelttrd  13148  xrltletrd  13149  xrletrd  13150  supxrunb1  13308  supxrunb2  13309  ixxun  13351  ixxss1  13353  ixxss2  13354  ixxss12  13355  fldiv4p1lem1div2  13831  fldiv4lem1div2uz2  13832  seqf1o  14042  faclbnd3  14291  relexpindlem  15062  01sqrexlem1  15241  01sqrexlem4  15244  01sqrexlem7  15247  abs3lemd  15463  rlimcn3  15589  o1of2  15612  lo1add  15626  lo1mul  15627  modfsummod  15794  mertenslem1  15886  sin01gt0  16194  cos01gt0  16195  sin02gt0  16196  dvds2addd  16298  dvds2subd  16299  dvdstrd  16301  bezoutlem4  16548  mulgcd  16554  lcmgcdeq  16618  mulgcddvds  16661  rpmulgcd2  16662  rpdvds  16666  divgcdcoprmex  16672  phimullem  16786  eulerthlem1  16788  eulerthlem2  16789  prmdiveq  16793  pythagtriplem4  16827  pcqmul  16861  pcgcd1  16885  pcadd  16897  pockthlem  16913  prmreclem2  16925  4sqlem16  16968  ramub1lem1  17034  ramub1lem2  17035  prmgaplem7  17065  iscatd2  17685  cicsym  17809  initoeu2  18021  joinval  18379  meetval  18393  lattrd  18450  latledi  18481  mulgass  19125  gaorber  19320  psgnunilem4  19509  efgredlem  19759  odadd2  19861  dmdprdpr  20063  ablfacrp2  20081  ablfac1b  20084  ablfac1eu  20087  pgpfac1  20094  orngmul  20883  gsumbagdiaglem  21952  mdetunilem1  22641  mdetunilem4  22644  mdetunilem9  22649  neiptoptop  23160  lmcnp  23333  txcls  23633  txlly  23665  txnlly  23666  tx1stc  23679  alexsubALTlem1  24076  prdsmet  24399  blin2  24458  blcvx  24827  tgqioo  24829  metnrmlem3  24891  iscmet3lem2  25323  ovolmge0  25508  ovolunlem2  25529  mbfi1flimlem  25753  mbfmullem  25756  itg2add  25790  dvferm1lem  26015  dvferm2lem  26017  dvlip2  26026  dvge0  26037  dvcvx  26051  dvfsumabs  26054  ftc1a  26068  plyadd  26246  plymul  26247  dgrlb  26265  plydivlem4  26326  vieta1lem2  26341  ulmdvlem3  26431  sinq12gt0  26538  logdivlti  26651  fsumharmonic  27042  mpodvdsmulf1o  27224  dvdsmulf1o  27226  logfacubnd  27251  perfectlem1  27259  dchrptlem2  27295  2sqlem5  27452  2sqlem8  27456  2sqmod  27466  dchrisum0flblem2  27539  pntibndlem2  27621  pntlemr  27632  pntlemp  27640  nosupbnd1  27744  nosupbnd2lem1  27745  nosupbnd2  27746  noinfbnd1  27759  noinfbnd2lem1  27760  noinfbnd2  27761  noetasuplem4  27766  noetainflem4  27770  ltstrd  27793  ltlestrd  27794  leltstrd  27795  lestrd  27796  oldbdayim  27948  mulsproplem5  28179  mulsproplem6  28180  mulsproplem7  28181  mulsproplem8  28182  ltmulsd  28196  bdayfinbndlem1  28526  bdayfinbnd  28528  axtgpasch  28602  tgjustr  28609  wlkcompim  29767  wwlksnredwwlkn  30030  wwlksnextsurj  30035  upgr4cycl4dv4e  30322  ex-natded5.2-2  30542  chscllem2  31776  chscllem4  31778  nmopge0  32049  nmfnge0  32065  nmoptrii  32232  staddi  32384  stadd3i  32386  atcvatlem  32523  xrofsup  32908  xrge0addgt0  33145  archiabllem2c  33325  linds2eq  33513  ssdifidlprm  33590  lbsdiflsp0  33867  fedgmullem2  33871  esumpmono  34320  unelldsys  34399  omssubaddlem  34540  signstfvneq0  34813  axtgupdim2ALTV  34909  bnj1098  35026  bnj1110  35224  bnj1121  35227  0nn0m1nnn0  35401  cplgredgex  35409  erdszelem8  35486  txsconn  35529  cvmlift2lem10  35600  cvmlift3lem7  35613  dfon2lem6  36074  dfon2lem8  36076  cgrtr4d  36273  cgrtrand  36281  cgrtr3and  36283  cgrextendand  36297  btwnexch3and  36309  btwnexchand  36314  linecgrand  36370  endofsegidand  36374  btwnconn1lem4  36378  btwnconn1lem8  36382  btwnconn1lem11  36385  btwnconn1lem12  36386  brsegle2  36397  seglecgr12im  36398  segleantisym  36403  colinbtwnle  36406  broutsideof2  36410  outsideoftr  36417  outsidele  36420  lineelsb2  36436  linethru  36441  gtinf  36617  weiunpo  36763  copsex2d  37569  relowlssretop  37795  pibt2  37849  heicant  38092  mbfresfi  38103  ftc1anclem6  38135  eqvreltrd  39129  riotasv2d  39519  lcvnbtwn2  39589  lcvnbtwn3  39590  lcvexchlem4  39599  omlfh1N  39820  atlen0  39872  atlatmstc  39881  cvratlem  39983  lnnat  39989  2atlt  40001  athgt  40018  1cvratex  40035  ps-2  40040  llncmp  40084  llncvrlpln  40120  lplncmp  40124  lplncvrlvol  40178  lvolcmp  40179  dalemcea  40222  dalem-cly  40233  dalem10  40235  dalem17  40242  dalem25  40260  dalem38  40272  dalem44  40278  dalem55  40289  2atm2atN  40347  cdlema1N  40353  paddasslem5  40386  dalawlem3  40435  dalawlem7  40439  dalawlem11  40443  dalawlem12  40444  lhp0lt  40565  4atexlemc  40631  cdlemg33a  41268  cdlemg33  41273  cdlemk51  41515  dia2dimlem2  41627  dia2dimlem3  41628  dihmeetlem20N  41888  coprmdvds2d  42556  flt4lem2  43167  flt4lem5f  43177  ismrcd2  43218  pellqrex  43394  jm2.17b  43476  jm2.26lem3  43516  fnwe2lem2  43566  omabs2  43847  addrcom  44988  infxrunb2  45881  0ellimcdiv  46161  dvnprodlem1  46458  stoweidlem15  46527  stoweidlem26  46538  stoweidlem28  46540  stoweidlem32  46544  stoweidlem44  46556  meadjuni  46969  natglobalincr  47391  dfatcolem  47787  icceuelpart  47980  perfectALTVlem1  48281  bgoldbtbndlem2  48366  bgoldbtbndlem3  48367  copisnmnd  48729  assintopass  48774  lcoss  48996  islindeps2  49043  isldepslvec2  49045  isisod  49586  euendfunc  50085