Theorem mp2and 698

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 694	. 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  3729  ssnelpssd  4108  frpomin  6340  tfisi  7857  tfindsg2  7860  mposn  8102  frxp2  8143  smoord  8379  oelimcl  8614  oeeui  8616  nnawordex  8651  omabs  8665  naddssim  8699  naddel12  8714  ertrd  8734  en2prd  9064  omxpenlem  9089  ixpfi2  9366  oismo  9555  cantnflem1c  9702  cantnflem1  9704  cantnflem3  9706  infxpenc2  10037  isfin2-2  10334  axdc2lem  10463  r1limwun  10751  letrd  11393  lelttrd  11394  ltletrd  11396  lttrd  11397  le2addd  11855  le2subd  11856  ltleaddd  11857  leltaddd  11858  lt2subd  11860  ltmul12a  12092  lemul12ad  12178  lemul12bd  12179  lt2halvesd  12482  uzind  12676  uztrn  12862  xrlttrd  13162  xrlelttrd  13163  xrltletrd  13164  xrletrd  13165  supxrunb1  13322  supxrunb2  13323  ixxun  13364  ixxss1  13366  ixxss2  13367  ixxss12  13368  fldiv4p1lem1div2  13824  fldiv4lem1div2uz2  13825  seqf1o  14032  faclbnd3  14275  relexpindlem  15034  01sqrexlem1  15213  01sqrexlem4  15216  01sqrexlem7  15219  abs3lemd  15432  rlimcn3  15558  o1of2  15581  lo1add  15595  lo1mul  15596  modfsummod  15764  mertenslem1  15854  sin01gt0  16158  cos01gt0  16159  sin02gt0  16160  dvds2addd  16260  dvds2subd  16261  dvdstrd  16263  bezoutlem4  16509  mulgcd  16515  lcmgcdeq  16574  mulgcddvds  16617  rpmulgcd2  16618  rpdvds  16622  divgcdcoprmex  16628  phimullem  16739  eulerthlem1  16741  eulerthlem2  16742  prmdiveq  16746  pythagtriplem4  16779  pcqmul  16813  pcgcd1  16837  pcadd  16849  pockthlem  16865  prmreclem2  16877  4sqlem16  16920  ramub1lem1  16986  ramub1lem2  16987  prmgaplem7  17017  iscatd2  17652  cicsym  17778  initoeu2  17996  joinval  18360  meetval  18374  lattrd  18429  latledi  18460  mulgass  19057  gaorber  19250  psgnunilem4  19443  efgredlem  19693  odadd2  19795  dmdprdpr  19997  ablfacrp2  20015  ablfac1b  20018  ablfac1eu  20021  pgpfac1  20028  gsumbagdiaglemOLD  21859  gsumbagdiaglem  21862  mdetunilem1  22501  mdetunilem4  22504  mdetunilem9  22509  neiptoptop  23022  lmcnp  23195  txcls  23495  txlly  23527  txnlly  23528  tx1stc  23541  alexsubALTlem1  23938  prdsmet  24263  blin2  24322  blcvx  24701  tgqioo  24703  metnrmlem3  24764  iscmet3lem2  25207  ovolmge0  25393  ovolunlem2  25414  mbfi1flimlem  25639  mbfmullem  25642  itg2add  25676  dvferm1lem  25903  dvferm2lem  25905  dvlip2  25915  dvge0  25926  dvcvx  25940  dvfsumabs  25944  ftc1a  25959  plyadd  26138  plymul  26139  dgrlb  26157  plydivlem4  26218  vieta1lem2  26233  ulmdvlem3  26325  sinq12gt0  26429  logdivlti  26541  fsumharmonic  26931  mpodvdsmulf1o  27113  dvdsmulf1o  27115  logfacubnd  27141  perfectlem1  27149  dchrptlem2  27185  2sqlem5  27342  2sqlem8  27346  2sqmod  27356  dchrisum0flblem2  27429  pntibndlem2  27511  pntlemr  27522  pntlemp  27530  nosupbnd1  27634  nosupbnd2lem1  27635  nosupbnd2  27636  noinfbnd1  27649  noinfbnd2lem1  27650  noinfbnd2  27651  noetasuplem4  27656  noetainflem4  27660  slttrd  27679  sltletrd  27680  slelttrd  27681  sletrd  27682  oldbdayim  27802  mulsproplem5  28007  mulsproplem6  28008  mulsproplem7  28009  mulsproplem8  28010  sltmuld  28024  axtgpasch  28258  tgjustr  28265  wlkcompim  29433  wwlksnredwwlkn  29693  wwlksnextsurj  29698  upgr4cycl4dv4e  29982  ex-natded5.2-2  30202  chscllem2  31435  chscllem4  31437  nmopge0  31708  nmfnge0  31724  nmoptrii  31891  staddi  32043  stadd3i  32045  atcvatlem  32182  supssd  32475  infssd  32476  xrofsup  32521  xrge0addgt0  32729  archiabllem2c  32881  orngmul  32958  linds2eq  33036  lbsdiflsp0  33256  fedgmullem2  33260  esumpmono  33634  unelldsys  33713  omssubaddlem  33855  signstfvneq0  34140  axtgupdim2ALTV  34236  bnj1098  34350  bnj1110  34549  bnj1121  34552  0nn0m1nnn0  34658  cplgredgex  34666  erdszelem8  34744  txsconn  34787  cvmlift2lem10  34858  cvmlift3lem7  34871  sotrd  35295  dfon2lem6  35320  dfon2lem8  35322  cgrtr4d  35517  cgrtrand  35525  cgrtr3and  35527  cgrextendand  35541  btwnexch3and  35553  btwnexchand  35558  linecgrand  35614  endofsegidand  35618  btwnconn1lem4  35622  btwnconn1lem8  35626  btwnconn1lem11  35629  btwnconn1lem12  35630  brsegle2  35641  seglecgr12im  35642  segleantisym  35647  colinbtwnle  35650  broutsideof2  35654  outsideoftr  35661  outsidele  35664  lineelsb2  35680  linethru  35685  gtinf  35739  copsex2d  36554  relowlssretop  36778  pibt2  36832  heicant  37063  mbfresfi  37074  ftc1anclem6  37106  eqvreltrd  38017  riotasv2d  38366  lcvnbtwn2  38436  lcvnbtwn3  38437  lcvexchlem4  38446  omlfh1N  38667  atlen0  38719  atlatmstc  38728  cvratlem  38831  lnnat  38837  2atlt  38849  athgt  38866  1cvratex  38883  ps-2  38888  llncmp  38932  llncvrlpln  38968  lplncmp  38972  lplncvrlvol  39026  lvolcmp  39027  dalemcea  39070  dalem-cly  39081  dalem10  39083  dalem17  39090  dalem25  39108  dalem38  39120  dalem44  39126  dalem55  39137  2atm2atN  39195  cdlema1N  39201  paddasslem5  39234  dalawlem3  39283  dalawlem7  39287  dalawlem11  39291  dalawlem12  39292  lhp0lt  39413  4atexlemc  39479  cdlemg33a  40116  cdlemg33  40121  cdlemk51  40363  dia2dimlem2  40475  dia2dimlem3  40476  dihmeetlem20N  40736  coprmdvds2d  41409  flt4lem2  41993  flt4lem5f  42003  ismrcd2  42041  pellqrex  42221  jm2.17b  42304  jm2.26lem3  42344  fnwe2lem2  42397  omabs2  42684  addrcom  43835  infxrunb2  44673  0ellimcdiv  44960  stoweidlem15  45326  stoweidlem26  45337  stoweidlem28  45339  stoweidlem32  45343  stoweidlem44  45355  meadjuni  45768  natglobalincr  46186  dfatcolem  46558  icceuelpart  46699  perfectALTVlem1  46984  bgoldbtbndlem2  47069  bgoldbtbndlem3  47070  copisnmnd  47154  assintopass  47199  lcoss  47427  islindeps2  47474  isldepslvec2  47476  difmodm1lt  47518