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  3717  ssnelpssd  4088  sotrd  5584  frpomin  6326  fvf1pr  7295  tfisi  7848  tfindsg2  7851  mposn  8096  frxp2  8137  smoord  8373  oelimcl  8606  oeeui  8608  nnawordex  8643  omabs  8657  naddssim  8691  naddel12  8706  ertrd  8729  en2prd  9056  omxpenlem  9081  fodomfir  9334  ixpfi2  9356  oismo  9546  cantnflem1c  9693  cantnflem1  9695  cantnflem3  9697  infxpenc2  10028  isfin2-2  10325  axdc2lem  10454  r1limwun  10742  letrd  11384  lelttrd  11385  ltletrd  11387  lttrd  11388  le2addd  11848  le2subd  11849  ltleaddd  11850  leltaddd  11851  lt2subd  11853  ltmul12a  12089  lemul12ad  12176  lemul12bd  12177  lt2halvesd  12481  uzind  12677  uztrn  12862  xrlttrd  13167  xrlelttrd  13168  xrltletrd  13169  xrletrd  13170  supxrunb1  13327  supxrunb2  13328  ixxun  13369  ixxss1  13371  ixxss2  13372  ixxss12  13373  fldiv4p1lem1div2  13841  fldiv4lem1div2uz2  13842  seqf1o  14050  faclbnd3  14298  relexpindlem  15069  01sqrexlem1  15248  01sqrexlem4  15251  01sqrexlem7  15254  abs3lemd  15467  rlimcn3  15593  o1of2  15616  lo1add  15630  lo1mul  15631  modfsummod  15797  mertenslem1  15887  sin01gt0  16193  cos01gt0  16194  sin02gt0  16195  dvds2addd  16296  dvds2subd  16297  dvdstrd  16299  bezoutlem4  16546  mulgcd  16552  lcmgcdeq  16616  mulgcddvds  16659  rpmulgcd2  16660  rpdvds  16664  divgcdcoprmex  16670  phimullem  16783  eulerthlem1  16785  eulerthlem2  16786  prmdiveq  16790  pythagtriplem4  16824  pcqmul  16858  pcgcd1  16882  pcadd  16894  pockthlem  16910  prmreclem2  16922  4sqlem16  16965  ramub1lem1  17031  ramub1lem2  17032  prmgaplem7  17062  iscatd2  17678  cicsym  17802  initoeu2  18014  joinval  18372  meetval  18386  lattrd  18441  latledi  18472  mulgass  19079  gaorber  19276  psgnunilem4  19463  efgredlem  19713  odadd2  19815  dmdprdpr  20017  ablfacrp2  20035  ablfac1b  20038  ablfac1eu  20041  pgpfac1  20048  gsumbagdiaglem  21875  mdetunilem1  22535  mdetunilem4  22538  mdetunilem9  22543  neiptoptop  23054  lmcnp  23227  txcls  23527  txlly  23559  txnlly  23560  tx1stc  23573  alexsubALTlem1  23970  prdsmet  24294  blin2  24353  blcvx  24722  tgqioo  24724  metnrmlem3  24786  iscmet3lem2  25229  ovolmge0  25415  ovolunlem2  25436  mbfi1flimlem  25660  mbfmullem  25663  itg2add  25697  dvferm1lem  25925  dvferm2lem  25927  dvlip2  25937  dvge0  25948  dvcvx  25962  dvfsumabs  25966  ftc1a  25981  plyadd  26159  plymul  26160  dgrlb  26178  plydivlem4  26241  vieta1lem2  26256  ulmdvlem3  26348  sinq12gt0  26452  logdivlti  26565  fsumharmonic  26958  mpodvdsmulf1o  27140  dvdsmulf1o  27142  logfacubnd  27168  perfectlem1  27176  dchrptlem2  27212  2sqlem5  27369  2sqlem8  27373  2sqmod  27383  dchrisum0flblem2  27456  pntibndlem2  27538  pntlemr  27549  pntlemp  27557  nosupbnd1  27662  nosupbnd2lem1  27663  nosupbnd2  27664  noinfbnd1  27677  noinfbnd2lem1  27678  noinfbnd2  27679  noetasuplem4  27684  noetainflem4  27688  slttrd  27707  sltletrd  27708  slelttrd  27709  sletrd  27710  oldbdayim  27830  mulsproplem5  28049  mulsproplem6  28050  mulsproplem7  28051  mulsproplem8  28052  sltmuld  28066  axtgpasch  28378  tgjustr  28385  wlkcompim  29544  wwlksnredwwlkn  29809  wwlksnextsurj  29814  upgr4cycl4dv4e  30098  ex-natded5.2-2  30318  chscllem2  31551  chscllem4  31553  nmopge0  31824  nmfnge0  31840  nmoptrii  32007  staddi  32159  stadd3i  32161  atcvatlem  32298  supssd  32622  infssd  32623  xrofsup  32678  xrge0addgt0  32931  archiabllem2c  33111  orngmul  33243  linds2eq  33314  ssdifidlprm  33391  lbsdiflsp0  33582  fedgmullem2  33586  esumpmono  34018  unelldsys  34097  omssubaddlem  34239  signstfvneq0  34525  axtgupdim2ALTV  34621  bnj1098  34735  bnj1110  34934  bnj1121  34937  0nn0m1nnn0  35056  cplgredgex  35064  erdszelem8  35141  txsconn  35184  cvmlift2lem10  35255  cvmlift3lem7  35268  dfon2lem6  35727  dfon2lem8  35729  cgrtr4d  35924  cgrtrand  35932  cgrtr3and  35934  cgrextendand  35948  btwnexch3and  35960  btwnexchand  35965  linecgrand  36021  endofsegidand  36025  btwnconn1lem4  36029  btwnconn1lem8  36033  btwnconn1lem11  36036  btwnconn1lem12  36037  brsegle2  36048  seglecgr12im  36049  segleantisym  36054  colinbtwnle  36057  broutsideof2  36061  outsideoftr  36068  outsidele  36071  lineelsb2  36087  linethru  36092  gtinf  36258  weiunpo  36404  copsex2d  37078  relowlssretop  37302  pibt2  37356  heicant  37600  mbfresfi  37611  ftc1anclem6  37643  eqvreltrd  38547  riotasv2d  38896  lcvnbtwn2  38966  lcvnbtwn3  38967  lcvexchlem4  38976  omlfh1N  39197  atlen0  39249  atlatmstc  39258  cvratlem  39361  lnnat  39367  2atlt  39379  athgt  39396  1cvratex  39413  ps-2  39418  llncmp  39462  llncvrlpln  39498  lplncmp  39502  lplncvrlvol  39556  lvolcmp  39557  dalemcea  39600  dalem-cly  39611  dalem10  39613  dalem17  39620  dalem25  39638  dalem38  39650  dalem44  39656  dalem55  39667  2atm2atN  39725  cdlema1N  39731  paddasslem5  39764  dalawlem3  39813  dalawlem7  39817  dalawlem11  39821  dalawlem12  39822  lhp0lt  39943  4atexlemc  40009  cdlemg33a  40646  cdlemg33  40651  cdlemk51  40893  dia2dimlem2  41005  dia2dimlem3  41006  dihmeetlem20N  41266  coprmdvds2d  41936  flt4lem2  42595  flt4lem5f  42605  ismrcd2  42647  pellqrex  42827  jm2.17b  42910  jm2.26lem3  42950  fnwe2lem2  43000  omabs2  43281  addrcom  44425  infxrunb2  45323  0ellimcdiv  45608  dvnprodlem1  45905  stoweidlem15  45974  stoweidlem26  45985  stoweidlem28  45987  stoweidlem32  45991  stoweidlem44  46003  meadjuni  46416  natglobalincr  46836  dfatcolem  47212  icceuelpart  47368  perfectALTVlem1  47653  bgoldbtbndlem2  47738  bgoldbtbndlem3  47739  copisnmnd  48030  assintopass  48075  lcoss  48298  islindeps2  48345  isldepslvec2  48347  difmodm1lt  48388  isisod  48876  euendfunc  49196