Theorem mp2an 423

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 421	. 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  424  jaoi  706  mp3an  1327  barbara  2112  eqeq12i  2179  vtocl2  2781  spc2ev  2822  sbc2ie  3022  csbieb  3086  sseq12i  3170  uneq12i  3274  ineq12i  3321  ifssun  3534  nelpri  3600  ralpr  3631  rexpr  3632  preq12i  3658  dfop  3757  opeq12i  3763  breq12i  3991  mpteq2ia  4068  exmidundif  4185  exmidundifim  4186  opex  4207  opi2  4211  opth2  4218  opeqsn  4230  opeqpr  4231  uniop  4233  opelopaba  4244  braba  4245  opelopab  4249  brab  4250  opelopabaf  4251  unex  4419  snnex  4426  op1stb  4456  ifelpwun  4461  onun2i  4468  onsucssi  4483  ontriexmidim  4499  ontr2exmid  4502  onsucsssucexmid  4504  onsucelsucexmid  4507  opthreg  4533  tfis  4560  finds  4577  finds2  4578  nnregexmid  4598  xpeq12i  4626  opelvv  4654  eqrelriiv  4698  eqrelrdv  4700  xpss  4712  xpex  4719  relop  4754  brco  4775  opelcnv  4786  brcnv  4787  asymref  4989  codir  4992  ssrnres  5046  dmprop  5078  dfco2  5103  cossxp  5126  cocnvss  5129  coex  5149  funsn  5236  fnsn  5242  feq23i  5332  resasplitss  5367  fabex  5376  fvex  5506  xpsn  5661  fmptap  5675  opabex  5709  acexmidlemv  5840  oveq12i  5854  oprabid  5874  oprabss  5928  caovcom  5999  opabex3  6090  iunex  6091  oprabex  6096  ofmres  6104  op1st  6114  op2nd  6115  fo1st  6125  fo2nd  6126  mpoex  6182  1stconst  6189  2ndconst  6190  algrflem  6197  dftpos4  6231  tpostpos  6232  tpossym  6244  frecex  6362  frecfnom  6369  sucinc  6413  fnoei  6420  oeiexg  6421  nnacli  6450  nnmcli  6451  elec  6540  ecovcom  6608  ecovass  6610  ecovdi  6612  fnmap  6621  mapval  6626  elmap  6643  elpm  6645  elpm2  6646  map0  6655  ixpconst  6674  entri  6752  endisj  6790  xpcomco  6792  phplem2  6819  ssfiexmid  6842  domfiexmid  6844  unfiexmid  6883  unfiin  6891  inresflem  7025  casefun  7050  caserel  7052  caseinj  7054  omp1eomlem  7059  omp1eom  7060  endjusym  7061  djufun  7069  djuinj  7071  ctssdccl  7076  ctssdclemr  7077  nninfex  7086  infnninf  7088  fodjuomnilemdc  7108  ctssexmid  7114  exmidonfinlem  7149  dju1p1e2  7153  exmidfodomrlemr  7158  exmidfodomrlemrALT  7159  exmidaclem  7164  pw1dom2  7183  onntri35  7193  onntri45  7197  1lt2pi  7281  indpi  7283  1nq  7307  rec1nq  7336  1lt2nq  7347  ltaddnq  7348  halfnqq  7351  prarloclemarch2  7360  prarloclemlt  7434  prarloclemcalc  7443  genpelxp  7452  ltexprlempr  7549  recexprlempr  7573  cauappcvgprlemcl  7594  cauappcvgprlemladd  7599  caucvgprlemcl  7617  caucvgprprlemcl  7645  suplocexprlemell  7654  suplocexprlemdisj  7661  suplocexprlemub  7664  0r  7691  1sr  7692  m1r  7693  m1p1sr  7701  m1m1sr  7702  0lt1sr  7706  1ne0sr  7707  1idsr  7709  recexgt0sr  7714  prsradd  7727  caucvgsrlemoffres  7741  caucvgsr  7743  mappsrprg  7745  map2psrprg  7746  pitonnlem1p1  7787  pitonnlem2  7788  pitoregt0  7790  peano2nnnn  7794  axi2m1  7816  axprecex  7821  axcnre  7822  nnindnn  7834  nntopi  7835  0cn  7891  addcli  7903  mulcli  7904  mulcomi  7905  readdcli  7912  remulcli  7913  rexpssxrxp  7943  ltrelxr  7959  gtneii  7994  lttri3i  7996  letri3i  7997  ltnsymi  7998  lenlti  7999  ltlei  8000  mulgt0i  8008  mulgt0ii  8009  0lt1  8025  addcomi  8042  pncan3oi  8114  resubcli  8161  subcli  8174  pncan3i  8175  negsubi  8176  subnegi  8177  subeq0i  8178  neg11i  8179  negcon1i  8180  negcon2i  8181  mulneg1i  8302  mulneg2i  8303  mul2negi  8304  addgt0ii  8389  ltnegi  8391  lenegi  8392  ltnegcon2i  8393  lesub0i  8394  ltaddposi  8395  posdifi  8396  ltnegcon1i  8397  lenegcon1i  8398  subge0i  8399  1ap0  8488  ltapii  8533  recrecapi  8640  dividapi  8641  div0api  8642  rec11apii  8657  divdiv32api  8663  recgt0ii  8802  ltrecii  8813  ltdiv23ii  8822  sup3exmid  8852  nnssre  8861  nnind  8873  nnmulcli  8879  nnsubi  8897  0le2  8947  1lt3  9028  2lt4  9030  1lt4  9031  3lt5  9033  2lt5  9034  1lt5  9035  4lt6  9037  3lt6  9038  2lt6  9039  1lt6  9040  5lt7  9042  4lt7  9043  3lt7  9044  2lt7  9045  1lt7  9046  6lt8  9048  5lt8  9049  4lt8  9050  3lt8  9051  2lt8  9052  1lt8  9053  7lt9  9055  6lt9  9056  5lt9  9057  4lt9  9058  3lt9  9059  2lt9  9060  1lt9  9061  2muline0  9082  nn0addcli  9151  nn0mulcli  9152  nn0addge1i  9162  nn0addge2i  9163  dfz2  9263  halfnz  9287  9p1e10  9324  numnncl  9331  numltc  9347  le9lt10  9348  nummac  9366  8lt10  9453  7lt10  9454  6lt10  9455  5lt10  9456  4lt10  9457  3lt10  9458  2lt10  9459  1lt10  9460  eluzaddi  9492  eluzsubi  9493  eluz2nn  9504  eluz4eluz2  9505  uzuzle23  9509  eluzge3nn  9510  divfnzn  9559  elq  9560  qreccl  9580  xrltnr  9715  mnfltpnf  9721  xaddmnf1  9784  pnfaddmnf  9786  mnfaddpnf  9787  xrex  9792  xaddid1  9798  xsubge0  9817  xposdif  9818  xleaddadd  9823  elicc2i  9875  ioomax  9884  iccmax  9885  ioopos  9886  elxrge0  9914  iccshftri  9931  iccshftli  9933  iccdili  9935  icccntri  9937  unitssre  9941  fz10  9981  fzpreddisj  10006  fz0to4untppr  10059  dfrp2  10199  fldiv4p1lem1div2  10240  frecfzennn  10361  fnn0nninf  10372  fxnn0nninf  10373  0tonninf  10374  1tonninf  10375  m1expcl2  10477  m1expcl  10478  nn0expcli  10481  sqmuli  10537  cu2  10553  i3  10556  subsqi  10564  binom2subi  10570  bcpasc  10679  4bc2eq6  10687  hashinfom  10691  prhash2ex  10722  hashp1i  10723  rei  10841  imi  10842  readdi  10870  imaddi  10871  remuli  10872  immuli  10873  cjaddi  10874  cjmuli  10875  ipcni  10876  crrei  10878  crimi  10879  rexfiuz  10931  sqrt1  10988  sqrt4  10989  sqrt9  10990  abs1  11014  sqrtmulii  11076  abslti  11080  abslei  11081  abssubi  11092  absmuli  11093  sqabsaddi  11094  sqabssubi  11095  abstrii  11097  fimaxre2  11168  climz  11233  abscn2  11256  recn2  11258  imcn2  11259  climabs  11261  climre  11263  climim  11264  fsumcnv  11378  fsumrelem  11412  fsumre  11413  fsumim  11414  arisum2  11440  expcnv  11445  geo2sum2  11456  geo2lim  11457  0.999...  11462  geoihalfsum  11463  fprodcnv  11566  fprodge0  11578  fprodge1  11580  ege2le3  11612  ef0  11613  reeff1  11641  tan0  11672  ef01bndlem  11697  sin01bnd  11698  cos01bnd  11699  cos1bnd  11700  cos2bnd  11701  sin01gt0  11702  cos01gt0  11703  sin02gt0  11704  sincos1sgn  11705  sincos2sgn  11706  cos12dec  11708  egt2lt3  11720  epos  11721  ene1  11725  eap1  11726  3dvdsdec  11802  3dvds2dec  11803  odd2np1lem  11809  n2dvds1  11849  z4even  11853  ndvdsi  11870  flodddiv4  11871  gcd0val  11893  6gcd4e2  11928  3lcm2e6woprm  12018  6lcm4e12  12019  3lcm2e6  12092  sqrt2irrlem  12093  phimullem  12157  pockthi  12288  xpnnen  12327  xpomen  12328  ennnfonelemj0  12334  ennnfonelem0  12338  ennnfonelemhf1o  12346  exmidunben  12359  qnnen  12364  unct  12375  setscom  12434  strleun  12484  ismgm  12588  fn0g  12606  txtopi  12901  txunii  12904  upxp  12912  uptx  12914  cnmpt1st  12928  cnmpt2nd  12929  txswaphmeolem  12960  qtopbasss  13161  cnmet  13170  cnopncntop  13177  remet  13180  blssioo  13185  tgqioo  13187  tgioo2cntop  13189  divcnap  13195  abscncf  13212  recncf  13213  imcncf  13214  cjcncf  13215  mulc1cncf  13216  cncfcn1cntop  13221  cdivcncfap  13227  expcncf  13232  cnrehmeocntop  13233  limccnp2lem  13285  limccnp2cntop  13286  dvcnp2cntop  13303  dvaddxxbr  13305  dvmulxxbr  13306  dvcoapbr  13311  dvrecap  13317  dveflem  13327  dvef  13328  sincn  13330  coscn  13331  reeff1oleme  13333  reeff1o  13334  cosz12  13341  sin0pilem1  13342  sin0pilem2  13343  pipos  13349  sinhalfpilem  13352  sincosq1lem  13386  sincosq1sgn  13387  sincosq2sgn  13388  sincosq3sgn  13389  sincosq4sgn  13390  sinq12gt0  13391  cosq14gt0  13393  cosq23lt0  13394  coseq0q4123  13395  coseq00topi  13396  coseq0negpitopi  13397  tangtx  13399  sincos4thpi  13401  tan4thpi  13402  sincos6thpi  13403  pigt3  13405  cosordlem  13410  cosq34lt1  13411  cos02pilt1  13412  cos0pilt1  13413  ioocosf1o  13415  negpitopissre  13416  log1  13427  loge  13428  2logb9irr  13529  sqrt2cxp2logb9e3  13533  2logb9irrap  13535  lgsdir2lem2  13570  lgsdir2lem3  13571  2sqlem9  13600  2sqlem10  13601  ex-fl  13606  ex-ceil  13607  ex-bc  13610  ex-dvds  13611  ex-gcd  13612  bj-charfunbi  13693  bj-unex  13801  bj-nn0suc0  13832  bj-nntrans  13833  bj-nnelirr  13835  012of  13875  2o01f  13876  pwle2  13878  nnsf  13885  peano3nninf  13887  exmidsbthrlem  13901  sbthom  13905  isomninnlem  13909  iooref1o  13913  trilpolemisumle  13917  trilpolemeq1  13919  trilpolemlt1  13920  apdiff  13927  iswomninnlem  13928  iswomni0  13930  ismkvnnlem  13931  dceqnconst  13938  dcapnconst  13939  nconstwlpolemgt0  13942  taupi  13949