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 398

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 209  df-an 399

This theorem is referenced by:  reu2eqd  3729  ssnelpssd  4091  tfisi  7575  tfindsg2  7578  mposn  7800  smoord  8004  oelimcl  8228  oeeui  8230  nnawordex  8265  omabs  8276  ertrd  8307  omxpenlem  8620  ixpfi2  8824  oismo  9006  cantnflem1c  9152  cantnflem1  9154  cantnflem3  9156  infxpenc2  9450  isfin2-2  9743  axdc2lem  9872  r1limwun  10160  letrd  10799  lelttrd  10800  ltletrd  10802  lttrd  10803  le2addd  11261  le2subd  11262  ltleaddd  11263  leltaddd  11264  lt2subd  11266  ltmul12a  11498  lemul12ad  11584  lemul12bd  11585  lt2halvesd  11888  uzind  12077  uztrn  12264  xrlttrd  12555  xrlelttrd  12556  xrltletrd  12557  xrletrd  12558  supxrunb1  12715  supxrunb2  12716  ixxun  12757  ixxss1  12759  ixxss2  12760  ixxss12  12761  fldiv4p1lem1div2  13208  fldiv4lem1div2uz2  13209  seqf1o  13414  faclbnd3  13655  rtrclreclem3  14421  relexpindlem  14424  sqrlem1  14604  sqrlem4  14607  sqrlem7  14610  abs3lemd  14823  rlimcn2  14949  o1of2  14971  lo1add  14985  lo1mul  14986  modfsummod  15151  mertenslem1  15242  sin01gt0  15545  cos01gt0  15546  sin02gt0  15547  dvds2subd  15647  bitsmod  15787  sadaddlem  15817  bezoutlem4  15892  mulgcd  15898  gcddvdslcm  15948  lcmgcdeq  15958  lcmfunsnlem2lem2  15985  mulgcddvds  16001  rpmulgcd2  16002  rpdvds  16006  divgcdcoprmex  16012  isprm5  16053  rpexp  16066  phimullem  16118  eulerthlem1  16120  eulerthlem2  16121  prmdiveq  16125  pythagtriplem4  16158  pcpremul  16182  pcqmul  16192  pcdvdstr  16214  pcgcd1  16215  pcadd  16227  pockthlem  16243  prmreclem2  16255  4sqlem8  16283  4sqlem14  16296  4sqlem16  16298  ramub1lem1  16364  ramub1lem2  16365  prmdvdsprmop  16381  prmgaplem1  16387  prmgaplcmlem1  16389  prmgaplem7  16395  iscatd2  16954  cicsym  17076  initoeu2  17278  joinval  17617  meetval  17631  lattrd  17670  latledi  17701  mulgass  18266  gaorber  18440  psgnunilem4  18627  efgredlem  18875  odadd2  18971  dmdprdpr  19173  ablfacrp2  19191  ablfac1b  19194  ablfac1eu  19197  pgpfac1  19204  gsumbagdiaglem  20157  znunit  20712  mdetunilem1  21223  mdetunilem4  21226  mdetunilem9  21231  neiptoptop  21741  lmcnp  21914  txcls  22214  txlly  22246  txnlly  22247  tx1stc  22260  alexsubALTlem1  22657  prdsmet  22982  blin2  23041  blcvx  23408  tgqioo  23410  metnrmlem3  23471  iscmet3lem2  23897  ovolmge0  24080  ovolunlem2  24101  mbfi1flimlem  24325  mbfmullem  24328  itg2add  24362  dvferm1lem  24583  dvferm2lem  24585  dvlip2  24594  dvge0  24605  dvcvx  24619  dvfsumabs  24622  ftc1a  24636  plyadd  24809  plymul  24810  dgrlb  24828  plydivlem4  24887  vieta1lem2  24902  ulmdvlem3  24992  sinq12gt0  25095  logdivlti  25205  fsumharmonic  25591  fsumdvdsdiaglem  25762  dvdsmulf1o  25773  logfacubnd  25799  perfectlem1  25807  dchrptlem2  25843  lgsmod  25901  2sqlem3  25998  2sqlem5  26000  2sqlem8  26004  2sqmod  26014  dchrisum0flblem2  26087  pntibndlem2  26169  pntlemr  26180  pntlemp  26188  axtgpasch  26255  tgjustr  26262  wlkcompim  27415  wwlksnredwwlkn  27675  wwlksnextsurj  27680  upgr4cycl4dv4e  27966  ex-natded5.2-2  28186  chscllem2  29417  chscllem4  29419  nmopge0  29690  nmfnge0  29706  nmoptrii  29873  staddi  30025  stadd3i  30027  atcvatlem  30164  supssd  30447  infssd  30448  xrofsup  30494  xrge0addgt0  30680  archiabllem2c  30826  orngmul  30878  linds2eq  30943  lbsdiflsp0  31024  fedgmullem2  31028  esumpmono  31340  unelldsys  31419  omssubaddlem  31559  signstfvneq0  31844  axtgupdim2ALTV  31941  bnj1098  32057  bnj1110  32256  bnj1121  32259  0nn0m1nnn0  32353  cplgredgex  32369  erdszelem8  32447  txsconn  32490  cvmlift2lem10  32561  cvmlift3lem7  32574  dvdspw  32984  sotrd  33003  dfon2lem6  33035  dfon2lem8  33037  frpomin  33080  nosupbnd1  33216  nosupbnd2lem1  33217  nosupbnd2  33218  noetalem3  33221  slttrd  33240  sltletrd  33241  slelttrd  33242  sletrd  33243  cgrtr4d  33448  cgrtrand  33456  cgrtr3and  33458  cgrextendand  33472  btwnexch3and  33484  btwnexchand  33489  linecgrand  33545  endofsegidand  33549  btwnconn1lem4  33553  btwnconn1lem8  33557  btwnconn1lem11  33560  btwnconn1lem12  33561  brsegle2  33572  seglecgr12im  33573  segleantisym  33578  colinbtwnle  33581  broutsideof2  33585  outsideoftr  33592  outsidele  33595  lineelsb2  33611  linethru  33616  gtinf  33669  copsex2d  34433  relowlssretop  34646  pibt2  34700  heicant  34929  mbfresfi  34940  ftc1anclem6  34974  eqvreltrd  35845  riotasv2d  36095  lcvnbtwn2  36165  lcvnbtwn3  36166  lcvexchlem4  36175  omlfh1N  36396  atlen0  36448  atlatmstc  36457  cvratlem  36559  lnnat  36565  2atlt  36577  athgt  36594  1cvratex  36611  ps-2  36616  llncmp  36660  llncvrlpln  36696  lplncmp  36700  lplncvrlvol  36754  lvolcmp  36755  dalemcea  36798  dalem-cly  36809  dalem10  36811  dalem17  36818  dalem25  36836  dalem38  36848  dalem44  36854  dalem55  36865  2atm2atN  36923  cdlema1N  36929  paddasslem5  36962  dalawlem3  37011  dalawlem7  37015  dalawlem11  37019  dalawlem12  37020  lhp0lt  37141  4atexlemc  37207  cdlemg33a  37844  cdlemg33  37849  cdlemk51  38091  dia2dimlem2  38203  dia2dimlem3  38204  dihmeetlem20N  38464  ismrcd2  39303  pellqrex  39483  jm2.17b  39565  dvdsacongtr  39588  jm2.26lem3  39605  jm2.27a  39609  jm2.27c  39611  fnwe2lem2  39658  addrcom  40814  infxrunb2  41643  0ellimcdiv  41937  stoweidlem15  42307  stoweidlem26  42318  stoweidlem28  42320  stoweidlem32  42324  stoweidlem44  42336  meadjuni  42746  dfatcolem  43461  icceuelpart  43603  perfectALTVlem1  43893  bgoldbtbndlem2  43978  bgoldbtbndlem3  43979  copisnmnd  44083  assintopass  44128  lcoss  44498  islindeps2  44545  isldepslvec2  44547  difmodm1lt  44589