Theorem mp2an 422

Description: An inference based on modus ponens. (Contributed by NM, 13-Apr-1995.)

Hypotheses

Ref	Expression
mp2an.1	⊢ 𝜑
mp2an.2	⊢ 𝜓
mp2an.3	⊢ ((𝜑 ∧ 𝜓) → 𝜒)

Assertion

Ref	Expression
mp2an	⊢ 𝜒

Proof of Theorem mp2an

Step	Hyp	Ref	Expression
1		mp2an.2	. 2 ⊢ 𝜓
2		mp2an.1	. . 3 ⊢ 𝜑
3		mp2an.3	. . 3 ⊢ ((𝜑 ∧ 𝜓) → 𝜒)
4	2, 3	mpan 420	. 2 ⊢ (𝜓 → 𝜒)
5	1, 4	ax-mp 5	1 ⊢ 𝜒

Syntax hints:   → wi 4   ∧ wa 103

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia3 107

This theorem is referenced by:  mp4an  423  jaoi  705  mp3an  1315  barbara  2095  eqeq12i  2151  vtocl2  2736  spc2ev  2776  sbc2ie  2975  csbieb  3036  sseq12i  3120  uneq12i  3223  ineq12i  3270  nelpri  3546  ralpr  3573  rexpr  3574  preq12i  3600  dfop  3699  opeq12i  3705  breq12i  3933  mpteq2ia  4009  exmidundif  4124  exmidundifim  4125  opex  4146  opi2  4150  opth2  4157  opeqsn  4169  opeqpr  4170  uniop  4172  opelopaba  4183  braba  4184  opelopab  4188  brab  4189  opelopabaf  4190  unex  4357  snnex  4364  op1stb  4394  onun2i  4402  onsucssi  4417  ontr2exmid  4435  onsucsssucexmid  4437  onsucelsucexmid  4440  opthreg  4466  tfis  4492  finds  4509  finds2  4510  nnregexmid  4529  xpeq12i  4556  opelvv  4584  eqrelriiv  4628  eqrelrdv  4630  xpss  4642  xpex  4649  relop  4684  brco  4705  opelcnv  4716  brcnv  4717  asymref  4919  codir  4922  ssrnres  4976  dmprop  5008  dfco2  5033  cossxp  5056  cocnvss  5059  coex  5079  funsn  5166  fnsn  5172  feq23i  5262  resasplitss  5297  fabex  5306  fvex  5434  xpsn  5589  fmptap  5603  opabex  5637  acexmidlemv  5765  oveq12i  5779  oprabid  5796  oprabss  5850  caovcom  5921  opabex3  6013  iunex  6014  oprabex  6019  ofmres  6027  op1st  6037  op2nd  6038  fo1st  6048  fo2nd  6049  mpoex  6104  1stconst  6111  2ndconst  6112  algrflem  6119  dftpos4  6153  tpostpos  6154  tpossym  6166  frecex  6284  frecfnom  6291  sucinc  6334  fnoei  6341  oeiexg  6342  nnacli  6371  nnmcli  6372  elec  6461  ecovcom  6529  ecovass  6531  ecovdi  6533  fnmap  6542  mapval  6547  elmap  6564  elpm  6566  elpm2  6567  map0  6576  ixpconst  6595  entri  6673  endisj  6711  xpcomco  6713  phplem2  6740  ssfiexmid  6763  domfiexmid  6765  unfiexmid  6799  unfiin  6807  inresflem  6938  casefun  6963  caserel  6965  caseinj  6967  omp1eomlem  6972  omp1eom  6973  endjusym  6974  djufun  6982  djuinj  6984  ctssdccl  6989  ctssdclemr  6990  fodjuomnilemdc  7009  ctssexmid  7017  exmidonfinlem  7042  dju1p1e2  7046  exmidfodomrlemr  7051  exmidfodomrlemrALT  7052  exmidaclem  7057  1lt2pi  7141  indpi  7143  1nq  7167  rec1nq  7196  1lt2nq  7207  ltaddnq  7208  halfnqq  7211  prarloclemarch2  7220  prarloclemlt  7294  prarloclemcalc  7303  genpelxp  7312  ltexprlempr  7409  recexprlempr  7433  cauappcvgprlemcl  7454  cauappcvgprlemladd  7459  caucvgprlemcl  7477  caucvgprprlemcl  7505  suplocexprlemell  7514  suplocexprlemdisj  7521  suplocexprlemub  7524  0r  7551  1sr  7552  m1r  7553  m1p1sr  7561  m1m1sr  7562  0lt1sr  7566  1ne0sr  7567  1idsr  7569  recexgt0sr  7574  prsradd  7587  caucvgsrlemoffres  7601  caucvgsr  7603  mappsrprg  7605  map2psrprg  7606  pitonnlem1p1  7647  pitonnlem2  7648  pitoregt0  7650  peano2nnnn  7654  axi2m1  7676  axprecex  7681  axcnre  7682  nnindnn  7694  nntopi  7695  0cn  7751  addcli  7763  mulcli  7764  mulcomi  7765  readdcli  7772  remulcli  7773  rexpssxrxp  7803  ltrelxr  7818  gtneii  7852  lttri3i  7854  letri3i  7855  ltnsymi  7856  lenlti  7857  ltlei  7858  mulgt0i  7866  mulgt0ii  7867  0lt1  7882  addcomi  7899  pncan3oi  7971  resubcli  8018  subcli  8031  pncan3i  8032  negsubi  8033  subnegi  8034  subeq0i  8035  neg11i  8036  negcon1i  8037  negcon2i  8038  mulneg1i  8159  mulneg2i  8160  mul2negi  8161  addgt0ii  8246  ltnegi  8248  lenegi  8249  ltnegcon2i  8250  lesub0i  8251  ltaddposi  8252  posdifi  8253  ltnegcon1i  8254  lenegcon1i  8255  subge0i  8256  1ap0  8345  ltapii  8390  recrecapi  8497  dividapi  8498  div0api  8499  rec11apii  8514  divdiv32api  8520  recgt0ii  8658  ltrecii  8669  ltdiv23ii  8678  sup3exmid  8708  nnssre  8717  nnind  8729  nnmulcli  8735  nnsubi  8753  0le2  8803  1lt3  8884  2lt4  8886  1lt4  8887  3lt5  8889  2lt5  8890  1lt5  8891  4lt6  8893  3lt6  8894  2lt6  8895  1lt6  8896  5lt7  8898  4lt7  8899  3lt7  8900  2lt7  8901  1lt7  8902  6lt8  8904  5lt8  8905  4lt8  8906  3lt8  8907  2lt8  8908  1lt8  8909  7lt9  8911  6lt9  8912  5lt9  8913  4lt9  8914  3lt9  8915  2lt9  8916  1lt9  8917  2muline0  8938  nn0addcli  9007  nn0mulcli  9008  nn0addge1i  9018  nn0addge2i  9019  dfz2  9116  halfnz  9140  9p1e10  9177  numnncl  9184  numltc  9200  le9lt10  9201  nummac  9219  8lt10  9306  7lt10  9307  6lt10  9308  5lt10  9309  4lt10  9310  3lt10  9311  2lt10  9312  1lt10  9313  eluzaddi  9345  eluzsubi  9346  eluz2nn  9357  uzuzle23  9359  eluzge3nn  9360  divfnzn  9406  elq  9407  qreccl  9427  xrltnr  9559  mnfltpnf  9564  xaddmnf1  9624  pnfaddmnf  9626  mnfaddpnf  9627  xrex  9632  xaddid1  9638  xsubge0  9657  xposdif  9658  xleaddadd  9663  elicc2i  9715  ioomax  9724  iccmax  9725  ioopos  9726  elxrge0  9754  iccshftri  9771  iccshftli  9773  iccdili  9775  icccntri  9777  unitssre  9781  fz10  9819  fzpreddisj  9844  fldiv4p1lem1div2  10071  frecfzennn  10192  fnn0nninf  10203  fxnn0nninf  10204  0tonninf  10205  1tonninf  10206  m1expcl2  10308  m1expcl  10309  nn0expcli  10312  sqmuli  10368  cu2  10384  i3  10387  subsqi  10395  binom2subi  10400  bcpasc  10505  4bc2eq6  10513  hashinfom  10517  prhash2ex  10548  hashp1i  10549  rei  10664  imi  10665  readdi  10693  imaddi  10694  remuli  10695  immuli  10696  cjaddi  10697  cjmuli  10698  ipcni  10699  crrei  10701  crimi  10702  rexfiuz  10754  sqrt1  10811  sqrt4  10812  sqrt9  10813  abs1  10837  sqrtmulii  10899  abslti  10903  abslei  10904  abssubi  10915  absmuli  10916  sqabsaddi  10917  sqabssubi  10918  abstrii  10920  fimaxre2  10991  climz  11054  abscn2  11077  recn2  11079  imcn2  11080  climabs  11082  climre  11084  climim  11085  fsumcnv  11199  fsumrelem  11233  fsumre  11234  fsumim  11235  arisum2  11261  expcnv  11266  geo2sum2  11277  geo2lim  11278  0.999...  11283  geoihalfsum  11284  ege2le3  11366  ef0  11367  reeff1  11396  tan0  11427  ef01bndlem  11452  sin01bnd  11453  cos01bnd  11454  cos1bnd  11455  cos2bnd  11456  sin01gt0  11457  cos01gt0  11458  sin02gt0  11459  sincos1sgn  11460  sincos2sgn  11461  cos12dec  11463  egt2lt3  11475  epos  11476  ene1  11480  eap1  11481  3dvdsdec  11551  3dvds2dec  11552  odd2np1lem  11558  n2dvds1  11598  z4even  11602  ndvdsi  11619  flodddiv4  11620  gcd0val  11638  6gcd4e2  11672  3lcm2e6woprm  11756  6lcm4e12  11757  3lcm2e6  11827  sqrt2irrlem  11828  phimullem  11890  xpnnen  11896  xpomen  11897  ennnfonelemj0  11903  ennnfonelem0  11907  ennnfonelemhf1o  11915  exmidunben  11928  qnnen  11933  unct  11943  setscom  11988  strleun  12037  txtopi  12419  txunii  12422  upxp  12430  uptx  12432  cnmpt1st  12446  cnmpt2nd  12447  txswaphmeolem  12478  qtopbasss  12679  cnmet  12688  cnopncntop  12695  remet  12698  blssioo  12703  tgqioo  12705  tgioo2cntop  12707  divcnap  12713  abscncf  12730  recncf  12731  imcncf  12732  cjcncf  12733  mulc1cncf  12734  cncfcn1cntop  12739  cdivcncfap  12745  expcncf  12750  cnrehmeocntop  12751  limccnp2lem  12803  limccnp2cntop  12804  dvcnp2cntop  12821  dvaddxxbr  12823  dvmulxxbr  12824  dvcoapbr  12829  dvrecap  12835  dveflem  12844  dvef  12845  sincn  12847  coscn  12848  cosz12  12850  sin0pilem1  12851  sin0pilem2  12852  pipos  12858  sinhalfpilem  12861  sincosq1lem  12895  sincosq1sgn  12896  sincosq2sgn  12897  sincosq3sgn  12898  sincosq4sgn  12899  sinq12gt0  12900  cosq14gt0  12902  cosq23lt0  12903  coseq0q4123  12904  coseq00topi  12905  coseq0negpitopi  12906  tangtx  12908  sincos4thpi  12910  tan4thpi  12911  sincos6thpi  12912  pigt3  12914  cosordlem  12919  cosq34lt1  12920  cos02pilt1  12921  ex-fl  12926  ex-ceil  12927  ex-bc  12930  ex-dvds  12931  ex-gcd  12932  bj-unex  13106  bj-nn0suc0  13137  bj-nntrans  13138  bj-nnelirr  13140  pw1dom2  13179  pwle2  13182  nnsf  13188  peano3nninf  13190  nninfex  13194  exmidsbthrlem  13206  sbthom  13210  isomninnlem  13214  trilpolemisumle  13220  trilpolemeq1  13222  trilpolemlt1  13223  taupi  13228