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  3744  ssnelpssd  4124  frpomin  6362  fvf1pr  7326  tfisi  7879  tfindsg2  7882  mposn  8126  frxp2  8167  smoord  8403  oelimcl  8636  oeeui  8638  nnawordex  8673  omabs  8687  naddssim  8721  naddel12  8736  ertrd  8759  en2prd  9086  omxpenlem  9111  fodomfir  9365  ixpfi2  9387  oismo  9577  cantnflem1c  9724  cantnflem1  9726  cantnflem3  9728  infxpenc2  10059  isfin2-2  10356  axdc2lem  10485  r1limwun  10773  letrd  11415  lelttrd  11416  ltletrd  11418  lttrd  11419  le2addd  11879  le2subd  11880  ltleaddd  11881  leltaddd  11882  lt2subd  11884  ltmul12a  12120  lemul12ad  12207  lemul12bd  12208  lt2halvesd  12511  uzind  12707  uztrn  12893  xrlttrd  13197  xrlelttrd  13198  xrltletrd  13199  xrletrd  13200  supxrunb1  13357  supxrunb2  13358  ixxun  13399  ixxss1  13401  ixxss2  13402  ixxss12  13403  fldiv4p1lem1div2  13871  fldiv4lem1div2uz2  13872  seqf1o  14080  faclbnd3  14327  relexpindlem  15098  01sqrexlem1  15277  01sqrexlem4  15280  01sqrexlem7  15283  abs3lemd  15496  rlimcn3  15622  o1of2  15645  lo1add  15659  lo1mul  15660  modfsummod  15826  mertenslem1  15916  sin01gt0  16222  cos01gt0  16223  sin02gt0  16224  dvds2addd  16325  dvds2subd  16326  dvdstrd  16328  bezoutlem4  16575  mulgcd  16581  lcmgcdeq  16645  mulgcddvds  16688  rpmulgcd2  16689  rpdvds  16693  divgcdcoprmex  16699  phimullem  16812  eulerthlem1  16814  eulerthlem2  16815  prmdiveq  16819  pythagtriplem4  16852  pcqmul  16886  pcgcd1  16910  pcadd  16922  pockthlem  16938  prmreclem2  16950  4sqlem16  16993  ramub1lem1  17059  ramub1lem2  17060  prmgaplem7  17090  iscatd2  17725  cicsym  17851  initoeu2  18069  joinval  18434  meetval  18448  lattrd  18503  latledi  18534  mulgass  19141  gaorber  19338  psgnunilem4  19529  efgredlem  19779  odadd2  19881  dmdprdpr  20083  ablfacrp2  20101  ablfac1b  20104  ablfac1eu  20107  pgpfac1  20114  gsumbagdiaglem  21967  mdetunilem1  22633  mdetunilem4  22636  mdetunilem9  22641  neiptoptop  23154  lmcnp  23327  txcls  23627  txlly  23659  txnlly  23660  tx1stc  23673  alexsubALTlem1  24070  prdsmet  24395  blin2  24454  blcvx  24833  tgqioo  24835  metnrmlem3  24896  iscmet3lem2  25339  ovolmge0  25525  ovolunlem2  25546  mbfi1flimlem  25771  mbfmullem  25774  itg2add  25808  dvferm1lem  26036  dvferm2lem  26038  dvlip2  26048  dvge0  26059  dvcvx  26073  dvfsumabs  26077  ftc1a  26092  plyadd  26270  plymul  26271  dgrlb  26289  plydivlem4  26352  vieta1lem2  26367  ulmdvlem3  26459  sinq12gt0  26563  logdivlti  26676  fsumharmonic  27069  mpodvdsmulf1o  27251  dvdsmulf1o  27253  logfacubnd  27279  perfectlem1  27287  dchrptlem2  27323  2sqlem5  27480  2sqlem8  27484  2sqmod  27494  dchrisum0flblem2  27567  pntibndlem2  27649  pntlemr  27660  pntlemp  27668  nosupbnd1  27773  nosupbnd2lem1  27774  nosupbnd2  27775  noinfbnd1  27788  noinfbnd2lem1  27789  noinfbnd2  27790  noetasuplem4  27795  noetainflem4  27799  slttrd  27818  sltletrd  27819  slelttrd  27820  sletrd  27821  oldbdayim  27941  mulsproplem5  28160  mulsproplem6  28161  mulsproplem7  28162  mulsproplem8  28163  sltmuld  28177  axtgpasch  28489  tgjustr  28496  wlkcompim  29664  wwlksnredwwlkn  29924  wwlksnextsurj  29929  upgr4cycl4dv4e  30213  ex-natded5.2-2  30433  chscllem2  31666  chscllem4  31668  nmopge0  31939  nmfnge0  31955  nmoptrii  32122  staddi  32274  stadd3i  32276  atcvatlem  32413  supssd  32726  infssd  32727  xrofsup  32777  xrge0addgt0  33004  archiabllem2c  33184  orngmul  33312  linds2eq  33388  ssdifidlprm  33465  lbsdiflsp0  33653  fedgmullem2  33657  esumpmono  34059  unelldsys  34138  omssubaddlem  34280  signstfvneq0  34565  axtgupdim2ALTV  34661  bnj1098  34775  bnj1110  34974  bnj1121  34977  0nn0m1nnn0  35096  cplgredgex  35104  erdszelem8  35182  txsconn  35225  cvmlift2lem10  35296  cvmlift3lem7  35309  sotrd  35744  dfon2lem6  35769  dfon2lem8  35771  cgrtr4d  35966  cgrtrand  35974  cgrtr3and  35976  cgrextendand  35990  btwnexch3and  36002  btwnexchand  36007  linecgrand  36063  endofsegidand  36067  btwnconn1lem4  36071  btwnconn1lem8  36075  btwnconn1lem11  36078  btwnconn1lem12  36079  brsegle2  36090  seglecgr12im  36091  segleantisym  36096  colinbtwnle  36099  broutsideof2  36103  outsideoftr  36110  outsidele  36113  lineelsb2  36129  linethru  36134  gtinf  36301  weiunpo  36447  copsex2d  37121  relowlssretop  37345  pibt2  37399  heicant  37641  mbfresfi  37652  ftc1anclem6  37684  eqvreltrd  38589  riotasv2d  38938  lcvnbtwn2  39008  lcvnbtwn3  39009  lcvexchlem4  39018  omlfh1N  39239  atlen0  39291  atlatmstc  39300  cvratlem  39403  lnnat  39409  2atlt  39421  athgt  39438  1cvratex  39455  ps-2  39460  llncmp  39504  llncvrlpln  39540  lplncmp  39544  lplncvrlvol  39598  lvolcmp  39599  dalemcea  39642  dalem-cly  39653  dalem10  39655  dalem17  39662  dalem25  39680  dalem38  39692  dalem44  39698  dalem55  39709  2atm2atN  39767  cdlema1N  39773  paddasslem5  39806  dalawlem3  39855  dalawlem7  39859  dalawlem11  39863  dalawlem12  39864  lhp0lt  39985  4atexlemc  40051  cdlemg33a  40688  cdlemg33  40693  cdlemk51  40935  dia2dimlem2  41047  dia2dimlem3  41048  dihmeetlem20N  41308  coprmdvds2d  41982  flt4lem2  42633  flt4lem5f  42643  ismrcd2  42686  pellqrex  42866  jm2.17b  42949  jm2.26lem3  42989  fnwe2lem2  43039  omabs2  43321  addrcom  44470  infxrunb2  45317  0ellimcdiv  45604  dvnprodlem1  45901  stoweidlem15  45970  stoweidlem26  45981  stoweidlem28  45983  stoweidlem32  45987  stoweidlem44  45999  meadjuni  46412  natglobalincr  46830  dfatcolem  47204  icceuelpart  47360  perfectALTVlem1  47645  bgoldbtbndlem2  47730  bgoldbtbndlem3  47731  copisnmnd  48012  assintopass  48057  lcoss  48281  islindeps2  48328  isldepslvec2  48330  difmodm1lt  48371  isisod  48806