Theorem mp2and 695

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 691	. 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 206  df-an 396

This theorem is referenced by:  reu2eqd  3674  ssnelpssd  4051  frpomin  6240  tfisi  7693  tfindsg2  7696  mposn  7927  smoord  8180  oelimcl  8407  oeeui  8409  nnawordex  8444  omabs  8455  ertrd  8488  omxpenlem  8829  ixpfi2  9078  oismo  9260  cantnflem1c  9406  cantnflem1  9408  cantnflem3  9410  infxpenc2  9762  isfin2-2  10059  axdc2lem  10188  r1limwun  10476  letrd  11115  lelttrd  11116  ltletrd  11118  lttrd  11119  le2addd  11577  le2subd  11578  ltleaddd  11579  leltaddd  11580  lt2subd  11582  ltmul12a  11814  lemul12ad  11900  lemul12bd  11901  lt2halvesd  12204  uzind  12395  uztrn  12582  xrlttrd  12875  xrlelttrd  12876  xrltletrd  12877  xrletrd  12878  supxrunb1  13035  supxrunb2  13036  ixxun  13077  ixxss1  13079  ixxss2  13080  ixxss12  13081  fldiv4p1lem1div2  13536  fldiv4lem1div2uz2  13537  seqf1o  13745  faclbnd3  13987  relexpindlem  14755  sqrlem1  14935  sqrlem4  14938  sqrlem7  14941  abs3lemd  15154  rlimcn3  15280  o1of2  15303  lo1add  15317  lo1mul  15318  modfsummod  15487  mertenslem1  15577  sin01gt0  15880  cos01gt0  15881  sin02gt0  15882  dvds2addd  15982  dvds2subd  15983  dvdstrd  15985  bezoutlem4  16231  mulgcd  16237  lcmgcdeq  16298  mulgcddvds  16341  rpmulgcd2  16342  rpdvds  16346  divgcdcoprmex  16352  phimullem  16461  eulerthlem1  16463  eulerthlem2  16464  prmdiveq  16468  pythagtriplem4  16501  pcqmul  16535  pcgcd1  16559  pcadd  16571  pockthlem  16587  prmreclem2  16599  4sqlem16  16642  ramub1lem1  16708  ramub1lem2  16709  prmgaplem7  16739  iscatd2  17371  cicsym  17497  initoeu2  17712  joinval  18076  meetval  18090  lattrd  18145  latledi  18176  mulgass  18721  gaorber  18895  psgnunilem4  19086  efgredlem  19334  odadd2  19431  dmdprdpr  19633  ablfacrp2  19651  ablfac1b  19654  ablfac1eu  19657  pgpfac1  19664  gsumbagdiaglemOLD  21122  gsumbagdiaglem  21125  mdetunilem1  21742  mdetunilem4  21745  mdetunilem9  21750  neiptoptop  22263  lmcnp  22436  txcls  22736  txlly  22768  txnlly  22769  tx1stc  22782  alexsubALTlem1  23179  prdsmet  23504  blin2  23563  blcvx  23942  tgqioo  23944  metnrmlem3  24005  iscmet3lem2  24437  ovolmge0  24622  ovolunlem2  24643  mbfi1flimlem  24868  mbfmullem  24871  itg2add  24905  dvferm1lem  25129  dvferm2lem  25131  dvlip2  25140  dvge0  25151  dvcvx  25165  dvfsumabs  25168  ftc1a  25182  plyadd  25359  plymul  25360  dgrlb  25378  plydivlem4  25437  vieta1lem2  25452  ulmdvlem3  25542  sinq12gt0  25645  logdivlti  25756  fsumharmonic  26142  dvdsmulf1o  26324  logfacubnd  26350  perfectlem1  26358  dchrptlem2  26394  2sqlem5  26551  2sqlem8  26555  2sqmod  26565  dchrisum0flblem2  26638  pntibndlem2  26720  pntlemr  26731  pntlemp  26739  axtgpasch  26809  tgjustr  26816  wlkcompim  27979  wwlksnredwwlkn  28239  wwlksnextsurj  28244  upgr4cycl4dv4e  28528  ex-natded5.2-2  28748  chscllem2  29979  chscllem4  29981  nmopge0  30252  nmfnge0  30268  nmoptrii  30435  staddi  30587  stadd3i  30589  atcvatlem  30726  supssd  31023  infssd  31024  xrofsup  31069  xrge0addgt0  31279  archiabllem2c  31428  orngmul  31481  linds2eq  31554  lbsdiflsp0  31686  fedgmullem2  31690  esumpmono  32026  unelldsys  32105  omssubaddlem  32245  signstfvneq0  32530  axtgupdim2ALTV  32627  bnj1098  32742  bnj1110  32941  bnj1121  32944  0nn0m1nnn0  33050  cplgredgex  33061  erdszelem8  33139  txsconn  33182  cvmlift2lem10  33253  cvmlift3lem7  33266  sotrd  33711  dfon2lem6  33743  dfon2lem8  33745  frxp2  33770  frxp3  33776  naddssim  33816  nosupbnd1  33896  nosupbnd2lem1  33897  nosupbnd2  33898  noinfbnd1  33911  noinfbnd2lem1  33912  noinfbnd2  33913  noetasuplem4  33918  noetainflem4  33922  slttrd  33941  sltletrd  33942  slelttrd  33943  sletrd  33944  oldbdayim  34050  cgrtr4d  34266  cgrtrand  34274  cgrtr3and  34276  cgrextendand  34290  btwnexch3and  34302  btwnexchand  34307  linecgrand  34363  endofsegidand  34367  btwnconn1lem4  34371  btwnconn1lem8  34375  btwnconn1lem11  34378  btwnconn1lem12  34379  brsegle2  34390  seglecgr12im  34391  segleantisym  34396  colinbtwnle  34399  broutsideof2  34403  outsideoftr  34410  outsidele  34413  lineelsb2  34429  linethru  34434  gtinf  34487  copsex2d  35289  relowlssretop  35513  pibt2  35567  heicant  35791  mbfresfi  35802  ftc1anclem6  35834  eqvreltrd  36700  riotasv2d  36950  lcvnbtwn2  37020  lcvnbtwn3  37021  lcvexchlem4  37030  omlfh1N  37251  atlen0  37303  atlatmstc  37312  cvratlem  37414  lnnat  37420  2atlt  37432  athgt  37449  1cvratex  37466  ps-2  37471  llncmp  37515  llncvrlpln  37551  lplncmp  37555  lplncvrlvol  37609  lvolcmp  37610  dalemcea  37653  dalem-cly  37664  dalem10  37666  dalem17  37673  dalem25  37691  dalem38  37703  dalem44  37709  dalem55  37720  2atm2atN  37778  cdlema1N  37784  paddasslem5  37817  dalawlem3  37866  dalawlem7  37870  dalawlem11  37874  dalawlem12  37875  lhp0lt  37996  4atexlemc  38062  cdlemg33a  38699  cdlemg33  38704  cdlemk51  38946  dia2dimlem2  39058  dia2dimlem3  39059  dihmeetlem20N  39319  coprmdvds2d  39990  flt4lem2  40464  flt4lem5f  40474  ismrcd2  40501  pellqrex  40681  jm2.17b  40763  jm2.26lem3  40803  fnwe2lem2  40856  addrcom  42046  infxrunb2  42861  0ellimcdiv  43144  stoweidlem15  43510  stoweidlem26  43521  stoweidlem28  43523  stoweidlem32  43527  stoweidlem44  43539  meadjuni  43949  dfatcolem  44698  icceuelpart  44840  perfectALTVlem1  45125  bgoldbtbndlem2  45210  bgoldbtbndlem3  45211  copisnmnd  45315  assintopass  45360  lcoss  45729  islindeps2  45776  isldepslvec2  45778  difmodm1lt  45820