Theorem mp2and 711

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 707	. 2 ⊢ (𝜑 → (𝜒 → 𝜃))
5	1, 4	mpd 15	1 ⊢ (𝜑 → 𝜃)

Syntax hints:   → wi 4   ∧ wa 383

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 196  df-an 385

This theorem is referenced by:  reu2eqd  3370  ssnelpssd  3681  tfisi  6950  tfindsg2  6953  mpt2sn  7155  smoord  7349  oelimcl  7567  oeeui  7569  nnawordex  7604  omabs  7614  ertrd  7645  omxpenlem  7946  ixpfi2  8147  oismo  8328  cantnflem1c  8467  cantnflem1  8469  cantnflem3  8471  infxpenc2  8728  axdc2lem  9153  r1limwun  9437  letrd  10073  lelttrd  10074  ltletrd  10076  lttrd  10077  le2addd  10525  le2subd  10526  ltleaddd  10527  leltaddd  10528  lt2subd  10530  ltmul12a  10758  lemul12ad  10845  lemul12bd  10846  lt2halvesd  11157  uzind  11345  uztrn  11580  xrlttrd  11866  xrlelttrd  11867  xrltletrd  11868  xrletrd  11869  supxrunb1  12021  supxrunb2  12022  ixxun  12062  ixxss1  12064  ixxss2  12065  ixxss12  12066  fldiv4p1lem1div2  12498  fldiv4lem1div2uz2  12499  seqf1o  12704  faclbnd3  12941  rtrclreclem3  13648  sqrlem1  13831  sqrlem4  13834  sqrlem7  13837  abs3lemd  14048  rlimcn2  14169  o1of2  14191  lo1add  14205  lo1mul  14206  modfsummod  14367  mertenslem1  14455  sin01gt0  14759  cos01gt0  14760  sin02gt0  14761  dvds2subd  14855  bitsmod  14996  sadaddlem  15026  bezoutlem4  15097  mulgcd  15103  gcddvdslcm  15153  lcmgcdeq  15163  lcmfunsnlem2lem2  15190  mulgcddvds  15207  rpmulgcd2  15208  rpdvds  15212  divgcdcoprmex  15218  isprm5  15257  rpexp  15270  phimullem  15322  eulerthlem1  15324  eulerthlem2  15325  prmdiv  15328  prmdiveq  15329  pythagtriplem4  15362  pcpremul  15386  pcqmul  15396  pcdvdstr  15418  pcgcd1  15419  pcadd  15431  pockthlem  15447  prmreclem2  15459  4sqlem8  15487  4sqlem10  15489  4sqlem14  15500  4sqlem16  15502  ramub1lem1  15568  ramub1lem2  15569  prmdvdsprmop  15585  prmgaplem1  15591  prmgaplcmlem1  15593  prmgaplem7  15599  iscatd2  16165  cicsym  16287  initoeu2  16489  joinval  16828  meetval  16842  lattrd  16881  latledi  16912  mulgass  17402  gaorber  17564  psgnunilem4  17740  efgredlem  17983  odadd2  18075  dmdprdpr  18271  ablfacrp2  18289  ablfac1b  18292  ablfac1eu  18295  pgpfac1  18302  gsumbagdiaglem  19196  znunit  19731  mdetunilem1  20237  mdetunilem4  20240  mdetunilem9  20245  neiptoptop  20745  lmcnp  20918  txcls  21217  txlly  21249  txnlly  21250  tx1stc  21263  alexsubALTlem1  21661  prdsmet  21985  blin2  22044  blcvx  22409  tgqioo  22411  metnrmlem3  22472  iscmet3lem2  22898  ovolmge0  23052  ovolunlem2  23073  mbfi1flimlem  23295  mbfmullem  23298  itg2add  23332  dvlip2  23562  dvge0  23573  dvcvx  23587  dvfsumabs  23590  plyadd  23777  plymul  23778  dgrlb  23796  plydivlem4  23855  vieta1lem2  23870  ulmdvlem3  23960  sinq12gt0  24063  logdivlti  24170  fsumharmonic  24538  fsumdvdsdiaglem  24709  dvdsmulf1o  24720  logfacubnd  24746  perfectlem1  24754  dchrptlem2  24790  lgsmod  24848  2sqlem3  24945  2sqlem5  24947  2sqlem8  24951  dchrisum0flblem2  24998  pntibndlem2  25080  pntlemr  25091  pntlemp  25099  axtgpasch  25166  wwlknredwwlkn  26254  wwlkextsur  26259  ex-natded5.2-2  26654  chscllem2  27881  chscllem4  27883  nmopge0  28154  nmfnge0  28170  nmoptrii  28337  staddi  28489  stadd3i  28491  atcvatlem  28628  supssd  28870  infssd  28871  xrofsup  28923  2sqmod  28979  xrge0addgt0  29022  archiabllem2c  29080  orngmul  29134  esumpmono  29468  unelldsys  29548  omssubaddlem  29688  signstfvneq0  29975  axtgupdim2OLD  29999  bnj1098  30108  bnj1110  30304  bnj1121  30307  erdszelem8  30434  txscon  30477  cvmlift2lem10  30548  cvmlift3lem7  30561  dvdspw  30889  dfon2lem6  30937  dfon2lem8  30939  cgrtr4d  31262  cgrtrand  31270  cgrtr3and  31272  cgrextendand  31286  btwnexch3and  31298  btwnexchand  31303  linecgrand  31359  endofsegidand  31363  btwnconn1lem4  31367  btwnconn1lem8  31371  btwnconn1lem11  31374  btwnconn1lem12  31375  brsegle2  31386  seglecgr12im  31387  segleantisym  31392  colinbtwnle  31395  broutsideof2  31399  outsideoftr  31406  outsidele  31409  lineelsb2  31425  linethru  31430  gtinf  31483  gtinfOLD  31484  relowlssretop  32387  heicant  32614  mbfresfi  32626  ftc1anclem6  32660  riotasv2d  33261  lcvnbtwn2  33332  lcvnbtwn3  33333  lcvexchlem4  33342  omlfh1N  33563  atlen0  33615  atlatmstc  33624  cvratlem  33725  lnnat  33731  2atlt  33743  athgt  33760  1cvratex  33777  ps-2  33782  llncmp  33826  llncvrlpln  33862  lplncmp  33866  lplncvrlvol  33920  lvolcmp  33921  dalemcea  33964  dalem-cly  33975  dalem10  33977  dalem17  33984  dalem25  34002  dalem38  34014  dalem44  34020  dalem55  34031  2atm2atN  34089  cdlema1N  34095  paddasslem5  34128  dalawlem3  34177  dalawlem7  34181  dalawlem11  34185  dalawlem12  34186  lhp0lt  34307  4atexlemc  34373  cdlemg33a  35012  cdlemg33  35017  cdlemk51  35259  dia2dimlem2  35372  dia2dimlem3  35373  dihmeetlem20N  35633  ismrcd2  36280  pellqrex  36461  jm2.17b  36546  dvdsacongtr  36569  jm2.26lem3  36586  jm2.27a  36590  jm2.27c  36592  fnwe2lem2  36639  fco2d  37481  addrcom  37700  infxrunb2  38525  0ellimcdiv  38716  stoweidlem15  38908  stoweidlem26  38919  stoweidlem28  38921  stoweidlem32  38925  stoweidlem44  38937  icceuelpart  39974  perfectALTVlem1  40164  bgoldbtbndlem2  40222  bgoldbtbndlem3  40223  1wlkcompim  40836  wwlksnredwwlkn  41101  wwlksnextsur  41106  upgr4cycl4dv4e  41352  copisnmnd  41599  assintopass  41640  lcoss  42019  islindeps2  42066  isldepslvec2  42068  difmodm1lt  42111