Theorem mp2an 426

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 424	. 2 ⊢ (𝜓 → 𝜒)
5	1, 4	ax-mp 5	1 ⊢ 𝜒

Syntax hints:   → wi 4   ∧ wa 104

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

This theorem is referenced by:  mp4an  427  jaoi  717  mp3an  1348  barbara  2140  eqeq12i  2207  vtocl2  2816  spc2ev  2857  sbc2ie  3058  csbieb  3123  sseq12i  3208  uneq12i  3312  ineq12i  3359  ifssun  3572  nelpri  3643  ralpr  3674  rexpr  3675  preq12i  3701  dfop  3804  opeq12i  3810  breq12i  4039  mpteq2ia  4116  exmidundif  4236  exmidundifim  4237  opex  4259  opi2  4263  opth2  4270  opeqsn  4282  opeqpr  4283  uniop  4285  opelopaba  4297  braba  4298  opelopab  4303  brab  4304  opelopabaf  4305  unex  4473  snnex  4480  op1stb  4510  ifelpwun  4515  ifex  4518  onun2i  4524  onsucssi  4539  ontriexmidim  4555  ontr2exmid  4558  onsucsssucexmid  4560  onsucelsucexmid  4563  opthreg  4589  tfis  4616  finds  4633  finds2  4634  nnregexmid  4654  xpeq12i  4682  opelvv  4710  eqrelriiv  4754  eqrelrdv  4756  xpss  4768  xpex  4775  relop  4813  brco  4834  opelcnv  4845  brcnv  4846  asymref  5052  codir  5055  ssrnres  5109  dmprop  5141  dfco2  5166  cossxp  5189  cocnvss  5192  coex  5212  funsn  5303  fnsn  5309  feq23i  5399  resasplitss  5434  fabex  5443  fvex  5575  xpsn  5735  fmptap  5749  opabex  5783  acexmidlemv  5917  oveq12i  5931  oprabid  5951  oprabss  6005  caovcom  6078  opabex3  6176  iunex  6177  oprabex  6182  ofmres  6190  op1st  6201  op2nd  6202  fo1st  6212  fo2nd  6213  mpoex  6269  1stconst  6276  2ndconst  6277  algrflem  6284  dftpos4  6318  tpostpos  6319  tpossym  6331  frecex  6449  frecfnom  6456  sucinc  6500  fnoei  6507  oeiexg  6508  nnacli  6537  nnmcli  6538  elec  6630  ecovcom  6698  ecovass  6700  ecovdi  6702  fnmap  6711  mapval  6716  elmap  6733  elpm  6735  elpm2  6736  map0  6745  ixpconst  6764  entri  6842  endisj  6880  xpcomco  6882  phplem2  6911  ssfiexmid  6934  domfiexmid  6936  exmidpw2en  6970  unfiexmid  6976  unfiin  6984  inresflem  7121  casefun  7146  caserel  7148  caseinj  7150  omp1eomlem  7155  omp1eom  7156  endjusym  7157  djufun  7165  djuinj  7167  ctssdccl  7172  ctssdclemr  7173  nninfex  7182  infnninf  7185  fodjuomnilemdc  7205  ctssexmid  7211  exmidonfinlem  7255  dju1p1e2  7259  exmidfodomrlemr  7264  exmidfodomrlemrALT  7265  exmidaclem  7270  pw1dom2  7289  onntri35  7299  onntri45  7303  2oneel  7318  2omotaplemst  7320  1lt2pi  7402  indpi  7404  1nq  7428  rec1nq  7457  1lt2nq  7468  ltaddnq  7469  halfnqq  7472  prarloclemarch2  7481  prarloclemlt  7555  prarloclemcalc  7564  genpelxp  7573  ltexprlempr  7670  recexprlempr  7694  cauappcvgprlemcl  7715  cauappcvgprlemladd  7720  caucvgprlemcl  7738  caucvgprprlemcl  7766  suplocexprlemell  7775  suplocexprlemdisj  7782  suplocexprlemub  7785  0r  7812  1sr  7813  m1r  7814  m1p1sr  7822  m1m1sr  7823  0lt1sr  7827  1ne0sr  7828  1idsr  7830  recexgt0sr  7835  prsradd  7848  caucvgsrlemoffres  7862  caucvgsr  7864  mappsrprg  7866  map2psrprg  7867  pitonnlem1p1  7908  pitonnlem2  7909  pitoregt0  7911  peano2nnnn  7915  axi2m1  7937  axprecex  7942  axcnre  7943  nnindnn  7955  nntopi  7956  0cn  8013  addcli  8025  mulcli  8026  mulcomi  8027  readdcli  8034  remulcli  8035  rexpssxrxp  8066  ltrelxr  8082  gtneii  8117  lttri3i  8119  letri3i  8120  ltnsymi  8121  lenlti  8122  ltlei  8123  mulgt0i  8131  mulgt0ii  8132  0lt1  8148  addcomi  8165  pncan3oi  8237  resubcli  8284  subcli  8297  pncan3i  8298  negsubi  8299  subnegi  8300  subeq0i  8301  neg11i  8302  negcon1i  8303  negcon2i  8304  mulneg1i  8425  mulneg2i  8426  mul2negi  8427  addgt0ii  8512  ltnegi  8514  lenegi  8515  ltnegcon2i  8516  lesub0i  8517  ltaddposi  8518  posdifi  8519  ltnegcon1i  8520  lenegcon1i  8521  subge0i  8522  1ap0  8611  ltapii  8656  recrecapi  8765  dividapi  8766  div0api  8767  rec11apii  8782  divdiv32api  8788  recgt0ii  8928  ltrecii  8939  ltdiv23ii  8948  sup3exmid  8978  nnssre  8988  nnind  9000  nnmulcli  9006  nnsubi  9024  0le2  9074  1lt3  9156  2lt4  9158  1lt4  9159  3lt5  9161  2lt5  9162  1lt5  9163  4lt6  9165  3lt6  9166  2lt6  9167  1lt6  9168  5lt7  9170  4lt7  9171  3lt7  9172  2lt7  9173  1lt7  9174  6lt8  9176  5lt8  9177  4lt8  9178  3lt8  9179  2lt8  9180  1lt8  9181  7lt9  9183  6lt9  9184  5lt9  9185  4lt9  9186  3lt9  9187  2lt9  9188  1lt9  9189  2muline0  9210  nn0addcli  9280  nn0mulcli  9281  nn0addge1i  9291  nn0addge2i  9292  dfz2  9392  halfnz  9416  9p1e10  9453  numnncl  9460  numltc  9476  le9lt10  9477  nummac  9495  8lt10  9582  7lt10  9583  6lt10  9584  5lt10  9585  4lt10  9586  3lt10  9587  2lt10  9588  1lt10  9589  eluzaddi  9622  eluzsubi  9623  eluz2nn  9634  eluz4eluz2  9635  uzuzle23  9639  eluzge3nn  9640  divfnzn  9689  elq  9690  qreccl  9710  xrltnr  9848  mnfltpnf  9854  xaddmnf1  9917  pnfaddmnf  9919  mnfaddpnf  9920  xrex  9925  xaddid1  9931  xsubge0  9950  xposdif  9951  xleaddadd  9956  elicc2i  10008  ioomax  10017  iccmax  10018  ioopos  10019  elxrge0  10047  iccshftri  10064  iccshftli  10066  iccdili  10068  icccntri  10070  unitssre  10074  fz10  10115  fzpreddisj  10140  fz0to4untppr  10193  dfrp2  10335  fldiv4p1lem1div2  10377  fldiv4lem1div2  10379  frecfzennn  10500  xnn0nnen  10511  fnn0nninf  10512  fxnn0nninf  10513  0tonninf  10514  1tonninf  10515  m1expcl2  10635  m1expcl  10636  nn0expcli  10639  sqmuli  10696  cu2  10712  i3  10715  subsqi  10723  binom2subi  10729  bcpasc  10840  4bc2eq6  10848  hashinfom  10852  prhash2ex  10883  hashp1i  10884  rei  11046  imi  11047  readdi  11075  imaddi  11076  remuli  11077  immuli  11078  cjaddi  11079  cjmuli  11080  ipcni  11081  crrei  11083  crimi  11084  rexfiuz  11136  sqrt1  11193  sqrt4  11194  sqrt9  11195  abs1  11219  sqrtmulii  11281  abslti  11285  abslei  11286  abssubi  11297  absmuli  11298  sqabsaddi  11299  sqabssubi  11300  abstrii  11302  fimaxre2  11373  climz  11438  abscn2  11461  recn2  11463  imcn2  11464  climabs  11466  climre  11468  climim  11469  fsumcnv  11583  fsumrelem  11617  fsumre  11618  fsumim  11619  arisum2  11645  expcnv  11650  geo2sum2  11661  geo2lim  11662  0.999...  11667  geoihalfsum  11668  fprodcnv  11771  fprodge0  11783  fprodge1  11785  ege2le3  11817  ef0  11818  reeff1  11846  tan0  11877  ef01bndlem  11902  sin01bnd  11903  cos01bnd  11904  cos1bnd  11905  cos2bnd  11906  sinltxirr  11907  sin01gt0  11908  cos01gt0  11909  sin02gt0  11910  sincos1sgn  11911  sincos2sgn  11912  cos12dec  11914  egt2lt3  11926  epos  11927  ene1  11931  eap1  11932  3dvdsdec  12009  3dvds2dec  12010  odd2np1lem  12016  n2dvds1  12056  z4even  12060  ndvdsi  12077  flodddiv4  12078  gcd0val  12100  6gcd4e2  12135  3lcm2e6woprm  12227  6lcm4e12  12228  3lcm2e6  12301  sqrt2irrlem  12302  phimullem  12366  pockthi  12499  4sqlem19  12550  xpnnen  12554  xpomen  12555  ennnfonelemj0  12561  ennnfonelem0  12565  ennnfonelemhf1o  12573  exmidunben  12586  qnnen  12591  unct  12602  setscom  12661  strleun  12725  prdsex  12883  imasival  12892  ismgm  12943  fn0g  12961  fngsum  12974  issgrp  12989  ismnddef  13002  isghm  13316  isrng  13433  rngmgpf  13436  isring  13499  mgpf  13510  dfrhm2  13653  rhmex  13656  isdomn  13768  rmodislmod  13850  lidlmex  13974  mopnset  14051  cnfldstr  14057  cnfldcj  14064  cnfld0  14070  cnfldplusf  14073  zringcrng  14091  zringmulr  14098  zringmpg  14105  znval  14135  psrval  14163  fnpsr  14164  txtopi  14440  txunii  14443  upxp  14451  uptx  14453  cnmpt1st  14467  cnmpt2nd  14468  txswaphmeolem  14499  qtopbasss  14700  cnmet  14709  cnfldms  14715  cnopncntop  14723  cnopn  14724  remet  14727  blssioo  14732  tgqioo  14734  tgioo2cntop  14736  tgioo2  14738  divcnap  14744  abscncf  14764  recncf  14765  imcncf  14766  cjcncf  14767  mulc1cncf  14768  cncfcn1cntop  14773  idcncf  14780  cdivcncfap  14783  expcncf  14788  cnrehmeocntop  14789  maxcncf  14794  mincncf  14795  ivthreinc  14824  hovercncf  14825  limccnp2lem  14855  limccnp2cntop  14856  dvcnp2cntop  14878  dvaddxxbr  14880  dvmulxxbr  14881  dvcoapbr  14886  dvrecap  14892  dveflem  14905  dvef  14906  sincn  14945  coscn  14946  reeff1oleme  14948  reeff1o  14949  cosz12  14956  sin0pilem1  14957  sin0pilem2  14958  pipos  14964  sinhalfpilem  14967  sincosq1lem  15001  sincosq1sgn  15002  sincosq2sgn  15003  sincosq3sgn  15004  sincosq4sgn  15005  sinq12gt0  15006  cosq14gt0  15008  cosq23lt0  15009  coseq0q4123  15010  coseq00topi  15011  coseq0negpitopi  15012  tangtx  15014  sincos4thpi  15016  tan4thpi  15017  sincos6thpi  15018  pigt3  15020  cosordlem  15025  cosq34lt1  15026  cos02pilt1  15027  cos0pilt1  15028  ioocosf1o  15030  negpitopissre  15031  log1  15042  loge  15043  2logb9irr  15144  sqrt2cxp2logb9e3  15148  2logb9irrap  15150  lgsdir2lem2  15186  lgsdir2lem3  15187  lgseisenlem4  15230  2lgsoddprmlem3  15268  2sqlem9  15281  2sqlem10  15282  ex-fl  15287  ex-ceil  15288  ex-bc  15291  ex-dvds  15292  ex-gcd  15293  bj-charfunbi  15373  bj-unex  15481  bj-nn0suc0  15512  bj-nntrans  15513  bj-nnelirr  15515  012of  15556  2o01f  15557  pwle2  15559  nnsf  15565  peano3nninf  15567  exmidsbthrlem  15582  sbthom  15586  isomninnlem  15590  iooref1o  15594  trilpolemisumle  15598  trilpolemeq1  15600  trilpolemlt1  15601  apdiff  15608  iswomninnlem  15609  iswomni0  15611  ismkvnnlem  15612  dceqnconst  15620  dcapnconst  15621  nconstwlpolemgt0  15624  taupi  15633