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 396

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 397

This theorem is referenced by:  reu2eqd  3697  ssnelpssd  4077  frpomin  6299  tfisi  7800  tfindsg2  7803  mposn  8040  frxp2  8081  smoord  8316  oelimcl  8552  oeeui  8554  nnawordex  8589  omabs  8602  naddssim  8636  naddel12  8651  ertrd  8671  en2prd  8999  omxpenlem  9024  ixpfi2  9301  oismo  9485  cantnflem1c  9632  cantnflem1  9634  cantnflem3  9636  infxpenc2  9967  isfin2-2  10264  axdc2lem  10393  r1limwun  10681  letrd  11321  lelttrd  11322  ltletrd  11324  lttrd  11325  le2addd  11783  le2subd  11784  ltleaddd  11785  leltaddd  11786  lt2subd  11788  ltmul12a  12020  lemul12ad  12106  lemul12bd  12107  lt2halvesd  12410  uzind  12604  uztrn  12790  xrlttrd  13088  xrlelttrd  13089  xrltletrd  13090  xrletrd  13091  supxrunb1  13248  supxrunb2  13249  ixxun  13290  ixxss1  13292  ixxss2  13293  ixxss12  13294  fldiv4p1lem1div2  13750  fldiv4lem1div2uz2  13751  seqf1o  13959  faclbnd3  14202  relexpindlem  14960  01sqrexlem1  15139  01sqrexlem4  15142  01sqrexlem7  15145  abs3lemd  15358  rlimcn3  15484  o1of2  15507  lo1add  15521  lo1mul  15522  modfsummod  15690  mertenslem1  15780  sin01gt0  16083  cos01gt0  16084  sin02gt0  16085  dvds2addd  16185  dvds2subd  16186  dvdstrd  16188  bezoutlem4  16434  mulgcd  16440  lcmgcdeq  16499  mulgcddvds  16542  rpmulgcd2  16543  rpdvds  16547  divgcdcoprmex  16553  phimullem  16662  eulerthlem1  16664  eulerthlem2  16665  prmdiveq  16669  pythagtriplem4  16702  pcqmul  16736  pcgcd1  16760  pcadd  16772  pockthlem  16788  prmreclem2  16800  4sqlem16  16843  ramub1lem1  16909  ramub1lem2  16910  prmgaplem7  16940  iscatd2  17575  cicsym  17701  initoeu2  17916  joinval  18280  meetval  18294  lattrd  18349  latledi  18380  mulgass  18927  gaorber  19102  psgnunilem4  19293  efgredlem  19543  odadd2  19641  dmdprdpr  19842  ablfacrp2  19860  ablfac1b  19863  ablfac1eu  19866  pgpfac1  19873  gsumbagdiaglemOLD  21377  gsumbagdiaglem  21380  mdetunilem1  21998  mdetunilem4  22001  mdetunilem9  22006  neiptoptop  22519  lmcnp  22692  txcls  22992  txlly  23024  txnlly  23025  tx1stc  23038  alexsubALTlem1  23435  prdsmet  23760  blin2  23819  blcvx  24198  tgqioo  24200  metnrmlem3  24261  iscmet3lem2  24693  ovolmge0  24878  ovolunlem2  24899  mbfi1flimlem  25124  mbfmullem  25127  itg2add  25161  dvferm1lem  25385  dvferm2lem  25387  dvlip2  25396  dvge0  25407  dvcvx  25421  dvfsumabs  25424  ftc1a  25438  plyadd  25615  plymul  25616  dgrlb  25634  plydivlem4  25693  vieta1lem2  25708  ulmdvlem3  25798  sinq12gt0  25901  logdivlti  26012  fsumharmonic  26398  dvdsmulf1o  26580  logfacubnd  26606  perfectlem1  26614  dchrptlem2  26650  2sqlem5  26807  2sqlem8  26811  2sqmod  26821  dchrisum0flblem2  26894  pntibndlem2  26976  pntlemr  26987  pntlemp  26995  nosupbnd1  27099  nosupbnd2lem1  27100  nosupbnd2  27101  noinfbnd1  27114  noinfbnd2lem1  27115  noinfbnd2  27116  noetasuplem4  27121  noetainflem4  27125  slttrd  27144  sltletrd  27145  slelttrd  27146  sletrd  27147  oldbdayim  27261  mulsproplem6  27427  mulsproplem7  27428  mulsproplem8  27429  mulsproplem9  27430  axtgpasch  27472  tgjustr  27479  wlkcompim  28643  wwlksnredwwlkn  28903  wwlksnextsurj  28908  upgr4cycl4dv4e  29192  ex-natded5.2-2  29412  chscllem2  30643  chscllem4  30645  nmopge0  30916  nmfnge0  30932  nmoptrii  31099  staddi  31251  stadd3i  31253  atcvatlem  31390  supssd  31694  infssd  31695  xrofsup  31740  xrge0addgt0  31952  archiabllem2c  32101  orngmul  32169  linds2eq  32241  lbsdiflsp0  32408  fedgmullem2  32412  esumpmono  32767  unelldsys  32846  omssubaddlem  32988  signstfvneq0  33273  axtgupdim2ALTV  33370  bnj1098  33484  bnj1110  33683  bnj1121  33686  0nn0m1nnn0  33792  cplgredgex  33801  erdszelem8  33879  txsconn  33922  cvmlift2lem10  33993  cvmlift3lem7  34006  sotrd  34424  dfon2lem6  34449  dfon2lem8  34451  cgrtr4d  34646  cgrtrand  34654  cgrtr3and  34656  cgrextendand  34670  btwnexch3and  34682  btwnexchand  34687  linecgrand  34743  endofsegidand  34747  btwnconn1lem4  34751  btwnconn1lem8  34755  btwnconn1lem11  34758  btwnconn1lem12  34759  brsegle2  34770  seglecgr12im  34771  segleantisym  34776  colinbtwnle  34779  broutsideof2  34783  outsideoftr  34790  outsidele  34793  lineelsb2  34809  linethru  34814  gtinf  34867  copsex2d  35683  relowlssretop  35907  pibt2  35961  heicant  36186  mbfresfi  36197  ftc1anclem6  36229  eqvreltrd  37143  riotasv2d  37492  lcvnbtwn2  37562  lcvnbtwn3  37563  lcvexchlem4  37572  omlfh1N  37793  atlen0  37845  atlatmstc  37854  cvratlem  37957  lnnat  37963  2atlt  37975  athgt  37992  1cvratex  38009  ps-2  38014  llncmp  38058  llncvrlpln  38094  lplncmp  38098  lplncvrlvol  38152  lvolcmp  38153  dalemcea  38196  dalem-cly  38207  dalem10  38209  dalem17  38216  dalem25  38234  dalem38  38246  dalem44  38252  dalem55  38263  2atm2atN  38321  cdlema1N  38327  paddasslem5  38360  dalawlem3  38409  dalawlem7  38413  dalawlem11  38417  dalawlem12  38418  lhp0lt  38539  4atexlemc  38605  cdlemg33a  39242  cdlemg33  39247  cdlemk51  39489  dia2dimlem2  39601  dia2dimlem3  39602  dihmeetlem20N  39862  coprmdvds2d  40532  flt4lem2  41043  flt4lem5f  41053  ismrcd2  41080  pellqrex  41260  jm2.17b  41343  jm2.26lem3  41383  fnwe2lem2  41436  omabs2  41725  addrcom  42877  infxrunb2  43723  0ellimcdiv  44010  stoweidlem15  44376  stoweidlem26  44387  stoweidlem28  44389  stoweidlem32  44393  stoweidlem44  44405  meadjuni  44818  natglobalincr  45236  dfatcolem  45607  icceuelpart  45748  perfectALTVlem1  46033  bgoldbtbndlem2  46118  bgoldbtbndlem3  46119  copisnmnd  46223  assintopass  46268  lcoss  46637  islindeps2  46684  isldepslvec2  46686  difmodm1lt  46728