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 399

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 210  df-an 400

This theorem is referenced by:  reu2eqd  3650  ssnelpssd  4018  tfisi  7572  tfindsg2  7575  mposn  7803  smoord  8012  oelimcl  8236  oeeui  8238  nnawordex  8273  omabs  8284  ertrd  8315  omxpenlem  8639  ixpfi2  8855  oismo  9037  cantnflem1c  9183  cantnflem1  9185  cantnflem3  9187  infxpenc2  9482  isfin2-2  9779  axdc2lem  9908  r1limwun  10196  letrd  10835  lelttrd  10836  ltletrd  10838  lttrd  10839  le2addd  11297  le2subd  11298  ltleaddd  11299  leltaddd  11300  lt2subd  11302  ltmul12a  11534  lemul12ad  11620  lemul12bd  11621  lt2halvesd  11922  uzind  12113  uztrn  12300  xrlttrd  12593  xrlelttrd  12594  xrltletrd  12595  xrletrd  12596  supxrunb1  12753  supxrunb2  12754  ixxun  12795  ixxss1  12797  ixxss2  12798  ixxss12  12799  fldiv4p1lem1div2  13254  fldiv4lem1div2uz2  13255  seqf1o  13461  faclbnd3  13702  relexpindlem  14470  sqrlem1  14650  sqrlem4  14653  sqrlem7  14656  abs3lemd  14869  rlimcn2  14995  o1of2  15017  lo1add  15031  lo1mul  15032  modfsummod  15197  mertenslem1  15288  sin01gt0  15591  cos01gt0  15592  sin02gt0  15593  dvds2addd  15693  dvds2subd  15694  dvdstrd  15696  bezoutlem4  15941  mulgcd  15947  lcmgcdeq  16008  mulgcddvds  16051  rpmulgcd2  16052  rpdvds  16056  divgcdcoprmex  16062  phimullem  16171  eulerthlem1  16173  eulerthlem2  16174  prmdiveq  16178  pythagtriplem4  16211  pcqmul  16245  pcgcd1  16268  pcadd  16280  pockthlem  16296  prmreclem2  16308  4sqlem16  16351  ramub1lem1  16417  ramub1lem2  16418  prmgaplem7  16448  iscatd2  17010  cicsym  17133  initoeu2  17342  joinval  17681  meetval  17695  lattrd  17734  latledi  17765  mulgass  18331  gaorber  18505  psgnunilem4  18692  efgredlem  18940  odadd2  19037  dmdprdpr  19239  ablfacrp2  19257  ablfac1b  19260  ablfac1eu  19263  pgpfac1  19270  gsumbagdiaglemOLD  20700  gsumbagdiaglem  20703  mdetunilem1  21312  mdetunilem4  21315  mdetunilem9  21320  neiptoptop  21831  lmcnp  22004  txcls  22304  txlly  22336  txnlly  22337  tx1stc  22350  alexsubALTlem1  22747  prdsmet  23072  blin2  23131  blcvx  23499  tgqioo  23501  metnrmlem3  23562  iscmet3lem2  23992  ovolmge0  24177  ovolunlem2  24198  mbfi1flimlem  24422  mbfmullem  24425  itg2add  24459  dvferm1lem  24683  dvferm2lem  24685  dvlip2  24694  dvge0  24705  dvcvx  24719  dvfsumabs  24722  ftc1a  24736  plyadd  24913  plymul  24914  dgrlb  24932  plydivlem4  24991  vieta1lem2  25006  ulmdvlem3  25096  sinq12gt0  25199  logdivlti  25310  fsumharmonic  25696  dvdsmulf1o  25878  logfacubnd  25904  perfectlem1  25912  dchrptlem2  25948  2sqlem5  26105  2sqlem8  26109  2sqmod  26119  dchrisum0flblem2  26192  pntibndlem2  26274  pntlemr  26285  pntlemp  26293  axtgpasch  26360  tgjustr  26367  wlkcompim  27520  wwlksnredwwlkn  27780  wwlksnextsurj  27785  upgr4cycl4dv4e  28069  ex-natded5.2-2  28289  chscllem2  29520  chscllem4  29522  nmopge0  29793  nmfnge0  29809  nmoptrii  29976  staddi  30128  stadd3i  30130  atcvatlem  30267  supssd  30568  infssd  30569  xrofsup  30614  xrge0addgt0  30826  archiabllem2c  30975  orngmul  31028  linds2eq  31096  lbsdiflsp0  31228  fedgmullem2  31232  esumpmono  31566  unelldsys  31645  omssubaddlem  31785  signstfvneq0  32070  axtgupdim2ALTV  32167  bnj1098  32283  bnj1110  32482  bnj1121  32485  0nn0m1nnn0  32579  cplgredgex  32598  erdszelem8  32676  txsconn  32719  cvmlift2lem10  32790  cvmlift3lem7  32803  sotrd  33248  dfon2lem6  33280  dfon2lem8  33282  frpomin  33325  frxp2  33346  frxp3  33352  naddssim  33422  nosupbnd1  33502  nosupbnd2lem1  33503  nosupbnd2  33504  noinfbnd1  33517  noinfbnd2lem1  33518  noinfbnd2  33519  noetasuplem4  33524  noetainflem4  33528  slttrd  33547  sltletrd  33548  slelttrd  33549  sletrd  33550  oldbdayim  33650  cgrtr4d  33858  cgrtrand  33866  cgrtr3and  33868  cgrextendand  33882  btwnexch3and  33894  btwnexchand  33899  linecgrand  33955  endofsegidand  33959  btwnconn1lem4  33963  btwnconn1lem8  33967  btwnconn1lem11  33970  btwnconn1lem12  33971  brsegle2  33982  seglecgr12im  33983  segleantisym  33988  colinbtwnle  33991  broutsideof2  33995  outsideoftr  34002  outsidele  34005  lineelsb2  34021  linethru  34026  gtinf  34079  copsex2d  34856  relowlssretop  35082  pibt2  35136  heicant  35394  mbfresfi  35405  ftc1anclem6  35437  eqvreltrd  36305  riotasv2d  36555  lcvnbtwn2  36625  lcvnbtwn3  36626  lcvexchlem4  36635  omlfh1N  36856  atlen0  36908  atlatmstc  36917  cvratlem  37019  lnnat  37025  2atlt  37037  athgt  37054  1cvratex  37071  ps-2  37076  llncmp  37120  llncvrlpln  37156  lplncmp  37160  lplncvrlvol  37214  lvolcmp  37215  dalemcea  37258  dalem-cly  37269  dalem10  37271  dalem17  37278  dalem25  37296  dalem38  37308  dalem44  37314  dalem55  37325  2atm2atN  37383  cdlema1N  37389  paddasslem5  37422  dalawlem3  37471  dalawlem7  37475  dalawlem11  37479  dalawlem12  37480  lhp0lt  37601  4atexlemc  37667  cdlemg33a  38304  cdlemg33  38309  cdlemk51  38551  dia2dimlem2  38663  dia2dimlem3  38664  dihmeetlem20N  38924  coprmdvds2d  39591  flt4lem2  39998  flt4lem5f  40008  ismrcd2  40035  pellqrex  40215  jm2.17b  40297  jm2.26lem3  40337  fnwe2lem2  40390  addrcom  41574  infxrunb2  42390  0ellimcdiv  42679  stoweidlem15  43045  stoweidlem26  43056  stoweidlem28  43058  stoweidlem32  43062  stoweidlem44  43074  meadjuni  43484  dfatcolem  44201  icceuelpart  44343  perfectALTVlem1  44628  bgoldbtbndlem2  44713  bgoldbtbndlem3  44714  copisnmnd  44818  assintopass  44863  lcoss  45232  islindeps2  45279  isldepslvec2  45281  difmodm1lt  45323