Theorem mp2and 712

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  reu2eqd  3693  ssnelpssd  4063  sotrd  5581  frpomin  6332  fvf1pr  7303  tfisi  7853  tfindsg2  7856  mposn  8097  frxp2  8139  smoord  8351  oelimcl  8587  oeeui  8589  nnawordex  8624  omabs  8638  naddssim  8673  naddel12  8688  ertrd  8712  en2prd  9053  omxpenlem  9075  fodomfir  9297  ixpfi2  9317  supssd  9433  infssd  9464  oismo  9512  cantnflem1c  9666  cantnflem1  9668  cantnflem3  9670  infxpenc2  10072  isfin2-2  10368  axdc2lem  10497  r1limwun  10792  letrd  11438  lelttrd  11439  ltletrd  11441  lttrd  11442  le2subd  11905  ltleaddd  11906  leltaddd  11907  lt2subd  11909  ltmul12a  12142  lemul12ad  12228  lemul12bd  12229  lt2halvesd  12563  0nn0m1nnn0  12722  uzind  12760  uztrn  12952  xrlttrd  13257  xrlelttrd  13258  xrltletrd  13259  xrletrd  13260  supxrunb1  13418  supxrunb2  13419  ixxun  13461  ixxss1  13463  ixxss2  13464  ixxss12  13465  fldiv4p1lem1div2  13943  fldiv4lem1div2uz2  13944  seqf1o  14154  faclbnd3  14403  relexpindlem  15183  01sqrexlem1  15376  01sqrexlem4  15379  01sqrexlem7  15382  abs3lemd  15598  rlimcn3  15724  o1of2  15747  lo1add  15761  lo1mul  15762  modfsummod  15928  mertenslem1  16020  sin01gt0  16325  cos01gt0  16326  sin02gt0  16327  dvds2addd  16429  dvds2subd  16430  dvdstrd  16432  bezoutlem4  16679  mulgcd  16685  lcmgcdeq  16749  mulgcddvds  16792  rpmulgcd2  16793  rpdvds  16797  divgcdcoprmex  16803  phimullem  16917  eulerthlem1  16919  eulerthlem2  16920  prmdiveq  16924  pythagtriplem4  16958  pcqmul  16992  pcgcd1  17016  pcadd  17028  pockthlem  17044  prmreclem2  17056  4sqlem16  17099  ramub1lem1  17165  ramub1lem2  17166  prmgaplem7  17196  iscatd2  17816  cicsym  17940  initoeu2  18152  joinval  18510  meetval  18524  lattrd  18581  latledi  18612  mulgass  19282  gaorber  19483  psgnunilem4  19672  efgredlem  19922  odadd2  20024  dmdprdpr  20226  ablfacrp2  20244  ablfac1b  20247  ablfac1eu  20250  pgpfac1  20257  orngmul  21083  ssdifidlprm  21603  gsumbagdiaglem  22200  mdetunilem1  22888  mdetunilem4  22891  mdetunilem9  22896  neiptoptop  23410  lmcnp  23583  txcls  23884  txlly  23916  txnlly  23917  tx1stc  23930  alexsubALTlem1  24327  prdsmet  24650  blin2  24709  blcvx  25078  tgqioo  25080  metnrmlem3  25142  iscmet3lem2  25574  ovolmge0  25759  ovolunlem2  25780  mbfi1flimlem  26004  mbfmullem  26007  itg2add  26041  dvferm1lem  26265  dvferm2lem  26267  dvlip2  26276  dvge0  26287  dvcvx  26301  dvfsumabs  26304  ftc1a  26318  plyadd  26497  plymul  26498  dgrlb  26516  plydivlem4  26580  vieta1lem2  26597  ulmdvlem3  26692  sinq12gt0  26799  logdivlti  26911  fsumharmonic  27302  mpodvdsmulf1o  27484  dvdsmulf1o  27486  logfacubnd  27511  perfectlem1  27519  dchrptlem2  27555  2sqlem5  27712  2sqlem8  27716  2sqmod  27726  dchrisum0flblem2  27799  pntibndlem2  27881  pntlemr  27892  pntlemp  27900  nosupbnd1  28004  nosupbnd2lem1  28005  nosupbnd2  28006  noinfbnd1  28019  noinfbnd2lem1  28020  noinfbnd2  28021  noetasuplem4  28026  noetainflem4  28030  ltstrd  28053  ltlestrd  28054  leltstrd  28055  lestrd  28056  oldbdayim  28208  mulsproplem5  28439  mulsproplem6  28440  mulsproplem7  28441  mulsproplem8  28442  ltmulsd  28456  bdayfinbndlem1  28786  bdayfinbnd  28788  axtgpasch  28862  tgjustr  28869  wlkcompim  30145  wwlksnredwwlkn  30417  wwlksnextsurj  30422  upgr4cycl4dv4e  30719  ex-natded5.2-2  30939  chscllem2  32173  chscllem4  32175  nmopge0  32446  nmfnge0  32462  nmoptrii  32629  staddi  32781  stadd3i  32783  atcvatlem  32920  xrofsup  33292  xrge0addgt0  33511  archiabllem2c  33689  linds2eq  33869  lbsdiflsp0  34191  fedgmullem2  34195  esumpmono  34644  unelldsys  34724  omssubaddlem  34865  signstfvneq0  35135  axtgupdim2ALTV  35231  bnj1098  35348  bnj1110  35546  bnj1121  35549  cplgredgex  35826  erdszelem8  35884  txsconn  35927  cvmlift2lem10  35998  cvmlift3lem7  36011  dfon2lem6  36472  dfon2lem8  36474  cgrtr4d  36672  cgrtrand  36680  cgrtr3and  36682  cgrextendand  36696  btwnexch3and  36708  btwnexchand  36713  linecgrand  36769  endofsegidand  36773  btwnconn1lem4  36777  btwnconn1lem8  36781  btwnconn1lem11  36784  btwnconn1lem12  36785  brsegle2  36796  seglecgr12im  36797  segleantisym  36802  colinbtwnle  36805  broutsideof2  36809  outsideoftr  36816  outsidele  36819  lineelsb2  36835  linethru  36840  ontr2d  36871  ltnadd  36889  gtinf  37029  weiunpo  37175  copsex2d  37980  relowlssretop  38206  pibt2  38260  heicant  38493  mbfresfi  38504  ftc1anclem6  38536  eqvreltrd  39544  riotasv2d  39934  lcvnbtwn2  40004  lcvnbtwn3  40005  lcvexchlem4  40014  omlfh1N  40235  atlen0  40287  atlatmstc  40296  cvratlem  40398  lnnat  40404  2atlt  40416  athgt  40433  1cvratex  40450  ps-2  40455  llncmp  40499  llncvrlpln  40535  lplncmp  40539  lplncvrlvol  40593  lvolcmp  40594  dalemcea  40637  dalem-cly  40648  dalem10  40650  dalem17  40657  dalem25  40675  dalem38  40687  dalem44  40693  dalem55  40704  2atm2atN  40762  cdlema1N  40768  paddasslem5  40801  dalawlem3  40850  dalawlem7  40854  dalawlem11  40858  dalawlem12  40859  lhp0lt  40980  4atexlemc  41046  cdlemg33a  41683  cdlemg33  41688  cdlemk51  41930  dia2dimlem2  42042  dia2dimlem3  42043  dihmeetlem20N  42303  coprmdvds2d  42971  flt4lem2  43597  flt4lem5f  43607  ismrcd2  43648  pellqrex  43824  jm2.17b  43906  jm2.26lem3  43946  fnwe2lem2  43996  omabs2  44277  addrcom  45401  infxrunb2  46301  0ellimcdiv  46581  dvnprodlem1  46878  stoweidlem15  46947  stoweidlem26  46958  stoweidlem28  46960  stoweidlem32  46964  stoweidlem44  46976  meadjuni  47389  dfatcolem  48247  icceuelpart  48440  perfectALTVlem1  48741  bgoldbtbndlem2  48826  bgoldbtbndlem3  48827  copisnmnd  49188  assintopass  49233  lcoss  49470  islindeps2  49517  isldepslvec2  49519  isisod  50057  euendfunc  50556