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  720  mp3an  1352  barbara  2156  eqeq12i  2223  el2v  2785  vtocl2  2836  spc2ev  2879  sbc2ie  3080  csbieb  3146  sseq12i  3232  uneq12i  3336  ineq12i  3383  ifssun  3597  nelpri  3670  ralpr  3701  rexpr  3702  preq12i  3728  dfop  3835  opeq12i  3841  breq12i  4071  mpteq2ia  4149  exmidundif  4269  exmidundifim  4270  opex  4294  opi2  4298  opth2  4305  opeqsn  4318  opeqpr  4319  uniop  4321  opelopaba  4333  braba  4334  opelopab  4339  brab  4340  opelopabaf  4341  unex  4509  snnex  4516  op1stb  4546  ifelpwun  4551  ifex  4554  onun2i  4560  onsucssi  4575  ontriexmidim  4591  ontr2exmid  4594  onsucsssucexmid  4596  onsucelsucexmid  4599  opthreg  4625  tfis  4652  finds  4669  finds2  4670  nnregexmid  4690  xpeq12i  4718  opelvv  4746  eqrelriiv  4790  eqrelrdv  4792  xpss  4804  xpex  4811  relop  4849  brco  4870  opelcnv  4881  brcnv  4882  asymref  5090  codir  5093  ssrnres  5147  dmprop  5179  dfco2  5204  cossxp  5227  cocnvss  5230  coex  5250  funsn  5345  fnsn  5351  feq23i  5444  resasplitss  5481  fabex  5490  fvex  5623  xpsn  5784  fmptap  5802  opabex  5836  acexmidlemv  5972  oveq12i  5986  oprabid  6006  oprabss  6061  caovcom  6134  opabex3  6237  iunex  6238  oprabex  6243  ofmres  6251  op1st  6262  op2nd  6263  fo1st  6273  fo2nd  6274  mpoex  6330  1stconst  6337  2ndconst  6338  algrflem  6345  dftpos4  6379  tpostpos  6380  tpossym  6392  frecex  6510  frecfnom  6517  sucinc  6561  fnoei  6568  oeiexg  6569  nnacli  6598  nnmcli  6599  elec  6691  ecovcom  6759  ecovass  6761  ecovdi  6763  fnmap  6772  mapval  6777  elmap  6794  elpm  6796  elpm2  6797  map0  6806  ixpconst  6825  entri  6908  endisj  6951  xpcomco  6953  phplem2  6982  1ndom2  6994  ssfiexmid  7006  domfiexmid  7008  exmidpw2en  7042  unfiexmid  7048  unfiin  7056  inresflem  7195  casefun  7220  caserel  7222  caseinj  7224  omp1eomlem  7229  omp1eom  7230  endjusym  7231  djufun  7239  djuinj  7241  ctssdccl  7246  ctssdclemr  7247  nninfex  7256  infnninf  7259  fodjuomnilemdc  7279  ctssexmid  7285  exmidonfinlem  7339  dju1p1e2  7343  exmidfodomrlemr  7348  exmidfodomrlemrALT  7349  exmidaclem  7358  pw1dom2  7380  onntri35  7390  onntri45  7394  2oneel  7410  2omotaplemst  7412  acnccim  7426  1lt2pi  7495  indpi  7497  1nq  7521  rec1nq  7550  1lt2nq  7561  ltaddnq  7562  halfnqq  7565  prarloclemarch2  7574  prarloclemlt  7648  prarloclemcalc  7657  genpelxp  7666  ltexprlempr  7763  recexprlempr  7787  cauappcvgprlemcl  7808  cauappcvgprlemladd  7813  caucvgprlemcl  7831  caucvgprprlemcl  7859  suplocexprlemell  7868  suplocexprlemdisj  7875  suplocexprlemub  7878  0r  7905  1sr  7906  m1r  7907  m1p1sr  7915  m1m1sr  7916  0lt1sr  7920  1ne0sr  7921  1idsr  7923  recexgt0sr  7928  prsradd  7941  caucvgsrlemoffres  7955  caucvgsr  7957  mappsrprg  7959  map2psrprg  7960  pitonnlem1p1  8001  pitonnlem2  8002  pitoregt0  8004  peano2nnnn  8008  axi2m1  8030  axprecex  8035  axcnre  8036  nnindnn  8048  nntopi  8049  0cn  8106  addcli  8118  mulcli  8119  mulcomi  8120  readdcli  8127  remulcli  8128  rexpssxrxp  8159  ltrelxr  8175  gtneii  8210  lttri3i  8212  letri3i  8213  ltnsymi  8214  lenlti  8215  ltlei  8216  mulgt0i  8224  mulgt0ii  8225  0lt1  8241  addcomi  8258  pncan3oi  8330  resubcli  8377  subcli  8390  pncan3i  8391  negsubi  8392  subnegi  8393  subeq0i  8394  neg11i  8395  negcon1i  8396  negcon2i  8397  mulneg1i  8518  mulneg2i  8519  mul2negi  8520  addgt0ii  8606  ltnegi  8608  lenegi  8609  ltnegcon2i  8610  lesub0i  8611  ltaddposi  8612  posdifi  8613  ltnegcon1i  8614  lenegcon1i  8615  subge0i  8616  1ap0  8705  ltapii  8750  recrecapi  8859  dividapi  8860  div0api  8861  rec11apii  8876  divdiv32api  8882  recgt0ii  9022  ltrecii  9033  ltdiv23ii  9042  sup3exmid  9072  nnssre  9082  nnind  9094  nnmulcli  9100  nnsubi  9118  0le2  9168  1lt3  9250  2lt4  9252  1lt4  9253  3lt5  9255  2lt5  9256  1lt5  9257  4lt6  9259  3lt6  9260  2lt6  9261  1lt6  9262  5lt7  9264  4lt7  9265  3lt7  9266  2lt7  9267  1lt7  9268  6lt8  9270  5lt8  9271  4lt8  9272  3lt8  9273  2lt8  9274  1lt8  9275  7lt9  9277  6lt9  9278  5lt9  9279  4lt9  9280  3lt9  9281  2lt9  9282  1lt9  9283  2muline0  9304  nn0addcli  9374  nn0mulcli  9375  nn0addge1i  9385  nn0addge2i  9386  dfz2  9487  halfnz  9511  9p1e10  9548  numnncl  9555  numltc  9571  le9lt10  9572  nummac  9590  8lt10  9677  7lt10  9678  6lt10  9679  5lt10  9680  4lt10  9681  3lt10  9682  2lt10  9683  1lt10  9684  eluzaddi  9717  eluzsubi  9718  eluz2nn  9729  eluz4eluz2  9730  uzuzle23  9734  eluzge3nn  9735  divfnzn  9784  elq  9785  qreccl  9805  xrltnr  9943  mnfltpnf  9949  xaddmnf1  10012  pnfaddmnf  10014  mnfaddpnf  10015  xrex  10020  xaddid1  10026  xsubge0  10045  xposdif  10046  xleaddadd  10051  elicc2i  10103  ioomax  10112  iccmax  10113  ioopos  10114  elxrge0  10142  iccshftri  10159  iccshftli  10161  iccdili  10163  icccntri  10165  unitssre  10169  fz10  10210  fzpreddisj  10235  fz0to4untppr  10288  dfrp2  10450  fldiv4p1lem1div2  10492  fldiv4lem1div2  10494  frecfzennn  10615  xnn0nnen  10626  fnn0nninf  10627  fxnn0nninf  10628  0tonninf  10629  1tonninf  10630  m1expcl2  10750  m1expcl  10751  nn0expcli  10754  sqmuli  10811  cu2  10827  i3  10830  subsqi  10838  binom2subi  10844  bcpasc  10955  4bc2eq6  10963  hashinfom  10967  prhash2ex  10998  hashp1i  10999  lsw0g  11086  swrdccat3blem  11237  rei  11376  imi  11377  readdi  11405  imaddi  11406  remuli  11407  immuli  11408  cjaddi  11409  cjmuli  11410  ipcni  11411  crrei  11413  crimi  11414  rexfiuz  11466  sqrt1  11523  sqrt4  11524  sqrt9  11525  abs1  11549  sqrtmulii  11611  abslti  11615  abslei  11616  abssubi  11627  absmuli  11628  sqabsaddi  11629  sqabssubi  11630  abstrii  11632  fimaxre2  11704  climz  11769  abscn2  11792  recn2  11794  imcn2  11795  climabs  11797  climre  11799  climim  11800  fsumcnv  11914  fsumrelem  11948  fsumre  11949  fsumim  11950  arisum2  11976  expcnv  11981  geo2sum2  11992  geo2lim  11993  0.999...  11998  geoihalfsum  11999  fprodcnv  12102  fprodge0  12114  fprodge1  12116  ege2le3  12148  ef0  12149  reeff1  12177  tan0  12208  ef01bndlem  12233  sin01bnd  12234  cos01bnd  12235  cos1bnd  12236  cos2bnd  12237  sinltxirr  12238  sin01gt0  12239  cos01gt0  12240  sin02gt0  12241  sincos1sgn  12242  sincos2sgn  12243  cos12dec  12245  egt2lt3  12257  epos  12258  ene1  12262  eap1  12263  3dvds  12341  3dvdsdec  12342  3dvds2dec  12343  odd2np1lem  12349  n2dvds1  12389  z4even  12393  ndvdsi  12410  flodddiv4  12413  bitsp1o  12430  0bits  12436  gcd0val  12447  6gcd4e2  12482  3lcm2e6woprm  12574  6lcm4e12  12575  3lcm2e6  12648  sqrt2irrlem  12649  phimullem  12713  pockthi  12847  4sqlem19  12898  dec2dvds  12900  dec5dvds2  12902  dec2nprm  12904  modxai  12905  gcdi  12909  gcdmodi  12910  numexpp1  12913  karatsuba  12919  2exp7  12923  xpnnen  12931  xpomen  12932  ennnfonelemj0  12938  ennnfonelem0  12942  ennnfonelemhf1o  12950  exmidunben  12963  qnnen  12968  unct  12979  setscom  13038  strleun  13103  prdsex  13268  prdsvallem  13271  imasival  13305  ismgm  13356  fn0g  13374  fngsum  13387  issgrp  13402  ismnddef  13417  isghm  13746  isrng  13863  rngmgpf  13866  isring  13929  mgpf  13940  dfrhm2  14083  rhmex  14086  isdomn  14198  rmodislmod  14280  lidlmex  14404  mopnset  14481  cnfldstr  14487  cnfldcj  14494  cnfld0  14500  cnfldplusf  14503  zringcrng  14521  zringmulr  14528  zringmpg  14535  znval  14565  psrval  14595  fnpsr  14596  fnmpl  14622  txtopi  14900  txunii  14903  upxp  14911  uptx  14913  cnmpt1st  14927  cnmpt2nd  14928  txswaphmeolem  14959  qtopbasss  15160  cnmet  15169  cnfldms  15175  cnopncntop  15183  cnopn  15184  remet  15187  blssioo  15192  tgqioo  15194  tgioo2cntop  15196  tgioo2  15198  divcnap  15204  abscncf  15224  recncf  15225  imcncf  15226  cjcncf  15227  mulc1cncf  15228  cncfcn1cntop  15233  idcncf  15240  cdivcncfap  15243  expcncf  15248  cnrehmeocntop  15249  maxcncf  15254  mincncf  15255  ivthreinc  15284  hovercncf  15285  limccnp2lem  15315  limccnp2cntop  15316  dvcnp2cntop  15338  dvaddxxbr  15340  dvmulxxbr  15341  dvcoapbr  15346  dvrecap  15352  dveflem  15365  dvef  15366  sincn  15408  coscn  15409  reeff1oleme  15411  reeff1o  15412  cosz12  15419  sin0pilem1  15420  sin0pilem2  15421  pipos  15427  sinhalfpilem  15430  sincosq1lem  15464  sincosq1sgn  15465  sincosq2sgn  15466  sincosq3sgn  15467  sincosq4sgn  15468  sinq12gt0  15469  cosq14gt0  15471  cosq23lt0  15472  coseq0q4123  15473  coseq00topi  15474  coseq0negpitopi  15475  tangtx  15477  sincos4thpi  15479  tan4thpi  15480  sincos6thpi  15481  pigt3  15483  cosordlem  15488  cosq34lt1  15489  cos02pilt1  15490  cos0pilt1  15491  ioocosf1o  15493  negpitopissre  15494  log1  15505  loge  15506  2logb9irr  15610  sqrt2cxp2logb9e3  15614  2logb9irrap  15616  mpodvdsmulf1o  15629  fsumdvdsmul  15630  1sgm2ppw  15634  lgsdir2lem2  15673  lgsdir2lem3  15674  lgseisenlem4  15717  2lgsoddprmlem3  15755  2sqlem9  15768  2sqlem10  15769  opvtxfvi  15793  opiedgfvi  15794  umgrbien  15875  ex-fl  15999  ex-ceil  16000  ex-bc  16003  ex-dvds  16004  ex-gcd  16005  bj-charfunbi  16084  bj-unex  16192  bj-nn0suc0  16223  bj-nntrans  16224  bj-nnelirr  16226  012of  16268  2o01f  16269  pwle2  16275  nnsf  16282  peano3nninf  16284  exmidsbthrlem  16301  sbthom  16305  isomninnlem  16309  iooref1o  16313  trilpolemisumle  16317  trilpolemeq1  16319  trilpolemlt1  16320  apdiff  16327  iswomninnlem  16328  iswomni0  16330  ismkvnnlem  16331  dceqnconst  16339  dcapnconst  16340  nconstwlpolemgt0  16343  taupi  16352