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 397

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 398

This theorem is referenced by:  reu2eqd  3733  ssnelpssd  4113  frpomin  6342  tfisi  7848  tfindsg2  7851  mposn  8089  frxp2  8130  smoord  8365  oelimcl  8600  oeeui  8602  nnawordex  8637  omabs  8650  naddssim  8684  naddel12  8699  ertrd  8719  en2prd  9048  omxpenlem  9073  ixpfi2  9350  oismo  9535  cantnflem1c  9682  cantnflem1  9684  cantnflem3  9686  infxpenc2  10017  isfin2-2  10314  axdc2lem  10443  r1limwun  10731  letrd  11371  lelttrd  11372  ltletrd  11374  lttrd  11375  le2addd  11833  le2subd  11834  ltleaddd  11835  leltaddd  11836  lt2subd  11838  ltmul12a  12070  lemul12ad  12156  lemul12bd  12157  lt2halvesd  12460  uzind  12654  uztrn  12840  xrlttrd  13138  xrlelttrd  13139  xrltletrd  13140  xrletrd  13141  supxrunb1  13298  supxrunb2  13299  ixxun  13340  ixxss1  13342  ixxss2  13343  ixxss12  13344  fldiv4p1lem1div2  13800  fldiv4lem1div2uz2  13801  seqf1o  14009  faclbnd3  14252  relexpindlem  15010  01sqrexlem1  15189  01sqrexlem4  15192  01sqrexlem7  15195  abs3lemd  15408  rlimcn3  15534  o1of2  15557  lo1add  15571  lo1mul  15572  modfsummod  15740  mertenslem1  15830  sin01gt0  16133  cos01gt0  16134  sin02gt0  16135  dvds2addd  16235  dvds2subd  16236  dvdstrd  16238  bezoutlem4  16484  mulgcd  16490  lcmgcdeq  16549  mulgcddvds  16592  rpmulgcd2  16593  rpdvds  16597  divgcdcoprmex  16603  phimullem  16712  eulerthlem1  16714  eulerthlem2  16715  prmdiveq  16719  pythagtriplem4  16752  pcqmul  16786  pcgcd1  16810  pcadd  16822  pockthlem  16838  prmreclem2  16850  4sqlem16  16893  ramub1lem1  16959  ramub1lem2  16960  prmgaplem7  16990  iscatd2  17625  cicsym  17751  initoeu2  17966  joinval  18330  meetval  18344  lattrd  18399  latledi  18430  mulgass  18991  gaorber  19172  psgnunilem4  19365  efgredlem  19615  odadd2  19717  dmdprdpr  19919  ablfacrp2  19937  ablfac1b  19940  ablfac1eu  19943  pgpfac1  19950  gsumbagdiaglemOLD  21491  gsumbagdiaglem  21494  mdetunilem1  22114  mdetunilem4  22117  mdetunilem9  22122  neiptoptop  22635  lmcnp  22808  txcls  23108  txlly  23140  txnlly  23141  tx1stc  23154  alexsubALTlem1  23551  prdsmet  23876  blin2  23935  blcvx  24314  tgqioo  24316  metnrmlem3  24377  iscmet3lem2  24809  ovolmge0  24994  ovolunlem2  25015  mbfi1flimlem  25240  mbfmullem  25243  itg2add  25277  dvferm1lem  25501  dvferm2lem  25503  dvlip2  25512  dvge0  25523  dvcvx  25537  dvfsumabs  25540  ftc1a  25554  plyadd  25731  plymul  25732  dgrlb  25750  plydivlem4  25809  vieta1lem2  25824  ulmdvlem3  25914  sinq12gt0  26017  logdivlti  26128  fsumharmonic  26516  dvdsmulf1o  26698  logfacubnd  26724  perfectlem1  26732  dchrptlem2  26768  2sqlem5  26925  2sqlem8  26929  2sqmod  26939  dchrisum0flblem2  27012  pntibndlem2  27094  pntlemr  27105  pntlemp  27113  nosupbnd1  27217  nosupbnd2lem1  27218  nosupbnd2  27219  noinfbnd1  27232  noinfbnd2lem1  27233  noinfbnd2  27234  noetasuplem4  27239  noetainflem4  27243  slttrd  27262  sltletrd  27263  slelttrd  27264  sletrd  27265  oldbdayim  27383  mulsproplem5  27576  mulsproplem6  27577  mulsproplem7  27578  mulsproplem8  27579  sltmuld  27593  axtgpasch  27718  tgjustr  27725  wlkcompim  28889  wwlksnredwwlkn  29149  wwlksnextsurj  29154  upgr4cycl4dv4e  29438  ex-natded5.2-2  29658  chscllem2  30891  chscllem4  30893  nmopge0  31164  nmfnge0  31180  nmoptrii  31347  staddi  31499  stadd3i  31501  atcvatlem  31638  supssd  31934  infssd  31935  xrofsup  31980  xrge0addgt0  32192  archiabllem2c  32341  orngmul  32421  linds2eq  32497  lbsdiflsp0  32711  fedgmullem2  32715  esumpmono  33077  unelldsys  33156  omssubaddlem  33298  signstfvneq0  33583  axtgupdim2ALTV  33680  bnj1098  33794  bnj1110  33993  bnj1121  33996  0nn0m1nnn0  34102  cplgredgex  34111  erdszelem8  34189  txsconn  34232  cvmlift2lem10  34303  cvmlift3lem7  34316  sotrd  34735  dfon2lem6  34760  dfon2lem8  34762  cgrtr4d  34957  cgrtrand  34965  cgrtr3and  34967  cgrextendand  34981  btwnexch3and  34993  btwnexchand  34998  linecgrand  35054  endofsegidand  35058  btwnconn1lem4  35062  btwnconn1lem8  35066  btwnconn1lem11  35069  btwnconn1lem12  35070  brsegle2  35081  seglecgr12im  35082  segleantisym  35087  colinbtwnle  35090  broutsideof2  35094  outsideoftr  35101  outsidele  35104  lineelsb2  35120  linethru  35125  gtinf  35204  copsex2d  36020  relowlssretop  36244  pibt2  36298  heicant  36523  mbfresfi  36534  ftc1anclem6  36566  eqvreltrd  37478  riotasv2d  37827  lcvnbtwn2  37897  lcvnbtwn3  37898  lcvexchlem4  37907  omlfh1N  38128  atlen0  38180  atlatmstc  38189  cvratlem  38292  lnnat  38298  2atlt  38310  athgt  38327  1cvratex  38344  ps-2  38349  llncmp  38393  llncvrlpln  38429  lplncmp  38433  lplncvrlvol  38487  lvolcmp  38488  dalemcea  38531  dalem-cly  38542  dalem10  38544  dalem17  38551  dalem25  38569  dalem38  38581  dalem44  38587  dalem55  38598  2atm2atN  38656  cdlema1N  38662  paddasslem5  38695  dalawlem3  38744  dalawlem7  38748  dalawlem11  38752  dalawlem12  38753  lhp0lt  38874  4atexlemc  38940  cdlemg33a  39577  cdlemg33  39582  cdlemk51  39824  dia2dimlem2  39936  dia2dimlem3  39937  dihmeetlem20N  40197  coprmdvds2d  40867  flt4lem2  41389  flt4lem5f  41399  ismrcd2  41437  pellqrex  41617  jm2.17b  41700  jm2.26lem3  41740  fnwe2lem2  41793  omabs2  42082  addrcom  43234  infxrunb2  44078  0ellimcdiv  44365  stoweidlem15  44731  stoweidlem26  44742  stoweidlem28  44744  stoweidlem32  44748  stoweidlem44  44760  meadjuni  45173  natglobalincr  45591  dfatcolem  45963  icceuelpart  46104  perfectALTVlem1  46389  bgoldbtbndlem2  46474  bgoldbtbndlem3  46475  copisnmnd  46579  assintopass  46624  lcoss  47117  islindeps2  47164  isldepslvec2  47166  difmodm1lt  47208