Theorem mp2and 697

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 693	. 2 ⊢ (𝜑 → (𝜒 → 𝜃))
5	1, 4	mpd 15	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:  reu2eqd  3676  ssnelpssd  4053  frpomin  6258  tfisi  7737  tfindsg2  7740  mposn  7975  smoord  8227  oelimcl  8462  oeeui  8464  nnawordex  8499  omabs  8512  ertrd  8545  en2prd  8873  omxpenlem  8898  ixpfi2  9161  oismo  9343  cantnflem1c  9489  cantnflem1  9491  cantnflem3  9493  infxpenc2  9824  isfin2-2  10121  axdc2lem  10250  r1limwun  10538  letrd  11178  lelttrd  11179  ltletrd  11181  lttrd  11182  le2addd  11640  le2subd  11641  ltleaddd  11642  leltaddd  11643  lt2subd  11645  ltmul12a  11877  lemul12ad  11963  lemul12bd  11964  lt2halvesd  12267  uzind  12458  uztrn  12646  xrlttrd  12939  xrlelttrd  12940  xrltletrd  12941  xrletrd  12942  supxrunb1  13099  supxrunb2  13100  ixxun  13141  ixxss1  13143  ixxss2  13144  ixxss12  13145  fldiv4p1lem1div2  13601  fldiv4lem1div2uz2  13602  seqf1o  13810  faclbnd3  14052  relexpindlem  14819  sqrlem1  14999  sqrlem4  15002  sqrlem7  15005  abs3lemd  15218  rlimcn3  15344  o1of2  15367  lo1add  15381  lo1mul  15382  modfsummod  15551  mertenslem1  15641  sin01gt0  15944  cos01gt0  15945  sin02gt0  15946  dvds2addd  16046  dvds2subd  16047  dvdstrd  16049  bezoutlem4  16295  mulgcd  16301  lcmgcdeq  16362  mulgcddvds  16405  rpmulgcd2  16406  rpdvds  16410  divgcdcoprmex  16416  phimullem  16525  eulerthlem1  16527  eulerthlem2  16528  prmdiveq  16532  pythagtriplem4  16565  pcqmul  16599  pcgcd1  16623  pcadd  16635  pockthlem  16651  prmreclem2  16663  4sqlem16  16706  ramub1lem1  16772  ramub1lem2  16773  prmgaplem7  16803  iscatd2  17435  cicsym  17561  initoeu2  17776  joinval  18140  meetval  18154  lattrd  18209  latledi  18240  mulgass  18785  gaorber  18959  psgnunilem4  19150  efgredlem  19398  odadd2  19495  dmdprdpr  19697  ablfacrp2  19715  ablfac1b  19718  ablfac1eu  19721  pgpfac1  19728  gsumbagdiaglemOLD  21186  gsumbagdiaglem  21189  mdetunilem1  21806  mdetunilem4  21809  mdetunilem9  21814  neiptoptop  22327  lmcnp  22500  txcls  22800  txlly  22832  txnlly  22833  tx1stc  22846  alexsubALTlem1  23243  prdsmet  23568  blin2  23627  blcvx  24006  tgqioo  24008  metnrmlem3  24069  iscmet3lem2  24501  ovolmge0  24686  ovolunlem2  24707  mbfi1flimlem  24932  mbfmullem  24935  itg2add  24969  dvferm1lem  25193  dvferm2lem  25195  dvlip2  25204  dvge0  25215  dvcvx  25229  dvfsumabs  25232  ftc1a  25246  plyadd  25423  plymul  25424  dgrlb  25442  plydivlem4  25501  vieta1lem2  25516  ulmdvlem3  25606  sinq12gt0  25709  logdivlti  25820  fsumharmonic  26206  dvdsmulf1o  26388  logfacubnd  26414  perfectlem1  26422  dchrptlem2  26458  2sqlem5  26615  2sqlem8  26619  2sqmod  26629  dchrisum0flblem2  26702  pntibndlem2  26784  pntlemr  26795  pntlemp  26803  axtgpasch  26873  tgjustr  26880  wlkcompim  28044  wwlksnredwwlkn  28305  wwlksnextsurj  28310  upgr4cycl4dv4e  28594  ex-natded5.2-2  28814  chscllem2  30045  chscllem4  30047  nmopge0  30318  nmfnge0  30334  nmoptrii  30501  staddi  30653  stadd3i  30655  atcvatlem  30792  supssd  31089  infssd  31090  xrofsup  31135  xrge0addgt0  31345  archiabllem2c  31494  orngmul  31547  linds2eq  31620  lbsdiflsp0  31752  fedgmullem2  31756  esumpmono  32092  unelldsys  32171  omssubaddlem  32311  signstfvneq0  32596  axtgupdim2ALTV  32693  bnj1098  32808  bnj1110  33007  bnj1121  33010  0nn0m1nnn0  33116  cplgredgex  33127  erdszelem8  33205  txsconn  33248  cvmlift2lem10  33319  cvmlift3lem7  33332  sotrd  33777  dfon2lem6  33809  dfon2lem8  33811  frxp2  33836  frxp3  33842  naddssim  33882  nosupbnd1  33962  nosupbnd2lem1  33963  nosupbnd2  33964  noinfbnd1  33977  noinfbnd2lem1  33978  noinfbnd2  33979  noetasuplem4  33984  noetainflem4  33988  slttrd  34007  sltletrd  34008  slelttrd  34009  sletrd  34010  oldbdayim  34116  cgrtr4d  34332  cgrtrand  34340  cgrtr3and  34342  cgrextendand  34356  btwnexch3and  34368  btwnexchand  34373  linecgrand  34429  endofsegidand  34433  btwnconn1lem4  34437  btwnconn1lem8  34441  btwnconn1lem11  34444  btwnconn1lem12  34445  brsegle2  34456  seglecgr12im  34457  segleantisym  34462  colinbtwnle  34465  broutsideof2  34469  outsideoftr  34476  outsidele  34479  lineelsb2  34495  linethru  34500  gtinf  34553  copsex2d  35354  relowlssretop  35578  pibt2  35632  heicant  35856  mbfresfi  35867  ftc1anclem6  35899  eqvreltrd  36763  riotasv2d  37013  lcvnbtwn2  37083  lcvnbtwn3  37084  lcvexchlem4  37093  omlfh1N  37314  atlen0  37366  atlatmstc  37375  cvratlem  37477  lnnat  37483  2atlt  37495  athgt  37512  1cvratex  37529  ps-2  37534  llncmp  37578  llncvrlpln  37614  lplncmp  37618  lplncvrlvol  37672  lvolcmp  37673  dalemcea  37716  dalem-cly  37727  dalem10  37729  dalem17  37736  dalem25  37754  dalem38  37766  dalem44  37772  dalem55  37783  2atm2atN  37841  cdlema1N  37847  paddasslem5  37880  dalawlem3  37929  dalawlem7  37933  dalawlem11  37937  dalawlem12  37938  lhp0lt  38059  4atexlemc  38125  cdlemg33a  38762  cdlemg33  38767  cdlemk51  39009  dia2dimlem2  39121  dia2dimlem3  39122  dihmeetlem20N  39382  coprmdvds2d  40052  flt4lem2  40521  flt4lem5f  40531  ismrcd2  40558  pellqrex  40738  jm2.17b  40821  jm2.26lem3  40861  fnwe2lem2  40914  addrcom  42131  infxrunb2  42955  0ellimcdiv  43239  stoweidlem15  43605  stoweidlem26  43616  stoweidlem28  43618  stoweidlem32  43622  stoweidlem44  43634  meadjuni  44045  dfatcolem  44805  icceuelpart  44946  perfectALTVlem1  45231  bgoldbtbndlem2  45316  bgoldbtbndlem3  45317  copisnmnd  45421  assintopass  45466  lcoss  45835  islindeps2  45882  isldepslvec2  45884  difmodm1lt  45926  natglobalincr  46570