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  27384  mulsproplem5  27579  mulsproplem6  27580  mulsproplem7  27581  mulsproplem8  27582  sltmuld  27596  axtgpasch  27749  tgjustr  27756  wlkcompim  28920  wwlksnredwwlkn  29180  wwlksnextsurj  29185  upgr4cycl4dv4e  29469  ex-natded5.2-2  29689  chscllem2  30922  chscllem4  30924  nmopge0  31195  nmfnge0  31211  nmoptrii  31378  staddi  31530  stadd3i  31532  atcvatlem  31669  supssd  31965  infssd  31966  xrofsup  32011  xrge0addgt0  32223  archiabllem2c  32372  orngmul  32452  linds2eq  32528  lbsdiflsp0  32742  fedgmullem2  32746  esumpmono  33108  unelldsys  33187  omssubaddlem  33329  signstfvneq0  33614  axtgupdim2ALTV  33711  bnj1098  33825  bnj1110  34024  bnj1121  34027  0nn0m1nnn0  34133  cplgredgex  34142  erdszelem8  34220  txsconn  34263  cvmlift2lem10  34334  cvmlift3lem7  34347  sotrd  34766  dfon2lem6  34791  dfon2lem8  34793  cgrtr4d  34988  cgrtrand  34996  cgrtr3and  34998  cgrextendand  35012  btwnexch3and  35024  btwnexchand  35029  linecgrand  35085  endofsegidand  35089  btwnconn1lem4  35093  btwnconn1lem8  35097  btwnconn1lem11  35100  btwnconn1lem12  35101  brsegle2  35112  seglecgr12im  35113  segleantisym  35118  colinbtwnle  35121  broutsideof2  35125  outsideoftr  35132  outsidele  35135  lineelsb2  35151  linethru  35156  gtinf  35252  copsex2d  36068  relowlssretop  36292  pibt2  36346  heicant  36571  mbfresfi  36582  ftc1anclem6  36614  eqvreltrd  37526  riotasv2d  37875  lcvnbtwn2  37945  lcvnbtwn3  37946  lcvexchlem4  37955  omlfh1N  38176  atlen0  38228  atlatmstc  38237  cvratlem  38340  lnnat  38346  2atlt  38358  athgt  38375  1cvratex  38392  ps-2  38397  llncmp  38441  llncvrlpln  38477  lplncmp  38481  lplncvrlvol  38535  lvolcmp  38536  dalemcea  38579  dalem-cly  38590  dalem10  38592  dalem17  38599  dalem25  38617  dalem38  38629  dalem44  38635  dalem55  38646  2atm2atN  38704  cdlema1N  38710  paddasslem5  38743  dalawlem3  38792  dalawlem7  38796  dalawlem11  38800  dalawlem12  38801  lhp0lt  38922  4atexlemc  38988  cdlemg33a  39625  cdlemg33  39630  cdlemk51  39872  dia2dimlem2  39984  dia2dimlem3  39985  dihmeetlem20N  40245  coprmdvds2d  40915  flt4lem2  41437  flt4lem5f  41447  ismrcd2  41485  pellqrex  41665  jm2.17b  41748  jm2.26lem3  41788  fnwe2lem2  41841  omabs2  42130  addrcom  43282  infxrunb2  44126  0ellimcdiv  44413  stoweidlem15  44779  stoweidlem26  44790  stoweidlem28  44792  stoweidlem32  44796  stoweidlem44  44808  meadjuni  45221  natglobalincr  45639  dfatcolem  46011  icceuelpart  46152  perfectALTVlem1  46437  bgoldbtbndlem2  46522  bgoldbtbndlem3  46523  copisnmnd  46627  assintopass  46672  lcoss  47165  islindeps2  47212  isldepslvec2  47214  difmodm1lt  47256