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  3675  ssnelpssd  4040  tfisi  7553  tfindsg2  7556  mposn  7781  smoord  7985  oelimcl  8209  oeeui  8211  nnawordex  8246  omabs  8257  ertrd  8288  omxpenlem  8601  ixpfi2  8806  oismo  8988  cantnflem1c  9134  cantnflem1  9136  cantnflem3  9138  infxpenc2  9433  isfin2-2  9730  axdc2lem  9859  r1limwun  10147  letrd  10786  lelttrd  10787  ltletrd  10789  lttrd  10790  le2addd  11248  le2subd  11249  ltleaddd  11250  leltaddd  11251  lt2subd  11253  ltmul12a  11485  lemul12ad  11571  lemul12bd  11572  lt2halvesd  11873  uzind  12062  uztrn  12249  xrlttrd  12540  xrlelttrd  12541  xrltletrd  12542  xrletrd  12543  supxrunb1  12700  supxrunb2  12701  ixxun  12742  ixxss1  12744  ixxss2  12745  ixxss12  12746  fldiv4p1lem1div2  13200  fldiv4lem1div2uz2  13201  seqf1o  13407  faclbnd3  13648  relexpindlem  14414  sqrlem1  14594  sqrlem4  14597  sqrlem7  14600  abs3lemd  14813  rlimcn2  14939  o1of2  14961  lo1add  14975  lo1mul  14976  modfsummod  15141  mertenslem1  15232  sin01gt0  15535  cos01gt0  15536  sin02gt0  15537  dvds2subd  15637  bitsmod  15775  sadaddlem  15805  bezoutlem4  15880  mulgcd  15886  gcddvdslcm  15936  lcmgcdeq  15946  lcmfunsnlem2lem2  15973  mulgcddvds  15989  rpmulgcd2  15990  rpdvds  15994  divgcdcoprmex  16000  isprm5  16041  rpexp  16054  phimullem  16106  eulerthlem1  16108  eulerthlem2  16109  prmdiveq  16113  pythagtriplem4  16146  pcpremul  16170  pcqmul  16180  pcdvdstr  16202  pcgcd1  16203  pcadd  16215  pockthlem  16231  prmreclem2  16243  4sqlem8  16271  4sqlem14  16284  4sqlem16  16286  ramub1lem1  16352  ramub1lem2  16353  prmdvdsprmop  16369  prmgaplem1  16375  prmgaplcmlem1  16377  prmgaplem7  16383  iscatd2  16944  cicsym  17066  initoeu2  17268  joinval  17607  meetval  17621  lattrd  17660  latledi  17691  mulgass  18256  gaorber  18430  psgnunilem4  18617  efgredlem  18865  odadd2  18962  dmdprdpr  19164  ablfacrp2  19182  ablfac1b  19185  ablfac1eu  19188  pgpfac1  19195  znunit  20255  gsumbagdiaglem  20613  mdetunilem1  21217  mdetunilem4  21220  mdetunilem9  21225  neiptoptop  21736  lmcnp  21909  txcls  22209  txlly  22241  txnlly  22242  tx1stc  22255  alexsubALTlem1  22652  prdsmet  22977  blin2  23036  blcvx  23403  tgqioo  23405  metnrmlem3  23466  iscmet3lem2  23896  ovolmge0  24081  ovolunlem2  24102  mbfi1flimlem  24326  mbfmullem  24329  itg2add  24363  dvferm1lem  24587  dvferm2lem  24589  dvlip2  24598  dvge0  24609  dvcvx  24623  dvfsumabs  24626  ftc1a  24640  plyadd  24814  plymul  24815  dgrlb  24833  plydivlem4  24892  vieta1lem2  24907  ulmdvlem3  24997  sinq12gt0  25100  logdivlti  25211  fsumharmonic  25597  fsumdvdsdiaglem  25768  dvdsmulf1o  25779  logfacubnd  25805  perfectlem1  25813  dchrptlem2  25849  lgsmod  25907  2sqlem3  26004  2sqlem5  26006  2sqlem8  26010  2sqmod  26020  dchrisum0flblem2  26093  pntibndlem2  26175  pntlemr  26186  pntlemp  26194  axtgpasch  26261  tgjustr  26268  wlkcompim  27421  wwlksnredwwlkn  27681  wwlksnextsurj  27686  upgr4cycl4dv4e  27970  ex-natded5.2-2  28190  chscllem2  29421  chscllem4  29423  nmopge0  29694  nmfnge0  29710  nmoptrii  29877  staddi  30029  stadd3i  30031  atcvatlem  30168  supssd  30471  infssd  30472  xrofsup  30518  xrge0addgt0  30725  archiabllem2c  30874  orngmul  30927  linds2eq  30995  lbsdiflsp0  31110  fedgmullem2  31114  esumpmono  31448  unelldsys  31527  omssubaddlem  31667  signstfvneq0  31952  axtgupdim2ALTV  32049  bnj1098  32165  bnj1110  32364  bnj1121  32367  0nn0m1nnn0  32461  cplgredgex  32480  erdszelem8  32558  txsconn  32601  cvmlift2lem10  32672  cvmlift3lem7  32685  dvdspw  33095  sotrd  33114  dfon2lem6  33146  dfon2lem8  33148  frpomin  33191  nosupbnd1  33327  nosupbnd2lem1  33328  nosupbnd2  33329  noetalem3  33332  slttrd  33351  sltletrd  33352  slelttrd  33353  sletrd  33354  cgrtr4d  33559  cgrtrand  33567  cgrtr3and  33569  cgrextendand  33583  btwnexch3and  33595  btwnexchand  33600  linecgrand  33656  endofsegidand  33660  btwnconn1lem4  33664  btwnconn1lem8  33668  btwnconn1lem11  33671  btwnconn1lem12  33672  brsegle2  33683  seglecgr12im  33684  segleantisym  33689  colinbtwnle  33692  broutsideof2  33696  outsideoftr  33703  outsidele  33706  lineelsb2  33722  linethru  33727  gtinf  33780  copsex2d  34554  relowlssretop  34780  pibt2  34834  heicant  35092  mbfresfi  35103  ftc1anclem6  35135  eqvreltrd  36003  riotasv2d  36253  lcvnbtwn2  36323  lcvnbtwn3  36324  lcvexchlem4  36333  omlfh1N  36554  atlen0  36606  atlatmstc  36615  cvratlem  36717  lnnat  36723  2atlt  36735  athgt  36752  1cvratex  36769  ps-2  36774  llncmp  36818  llncvrlpln  36854  lplncmp  36858  lplncvrlvol  36912  lvolcmp  36913  dalemcea  36956  dalem-cly  36967  dalem10  36969  dalem17  36976  dalem25  36994  dalem38  37006  dalem44  37012  dalem55  37023  2atm2atN  37081  cdlema1N  37087  paddasslem5  37120  dalawlem3  37169  dalawlem7  37173  dalawlem11  37177  dalawlem12  37178  lhp0lt  37299  4atexlemc  37365  cdlemg33a  38002  cdlemg33  38007  cdlemk51  38249  dia2dimlem2  38361  dia2dimlem3  38362  dihmeetlem20N  38622  dvdstrd  39285  coprmdvds2d  39290  ismrcd2  39640  pellqrex  39820  jm2.17b  39902  dvdsacongtr  39925  jm2.26lem3  39942  jm2.27a  39946  jm2.27c  39948  fnwe2lem2  39995  addrcom  41179  infxrunb2  42000  0ellimcdiv  42291  stoweidlem15  42657  stoweidlem26  42668  stoweidlem28  42670  stoweidlem32  42674  stoweidlem44  42686  meadjuni  43096  dfatcolem  43811  icceuelpart  43953  perfectALTVlem1  44239  bgoldbtbndlem2  44324  bgoldbtbndlem3  44325  copisnmnd  44429  assintopass  44474  lcoss  44845  islindeps2  44892  isldepslvec2  44894  difmodm1lt  44936