Theorem mp2an 420

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

Syntax hints:   → wi 4   ∧ wa 103

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

This theorem is referenced by:  mp4an  421  jaoi  677  mp3an  1283  barbara  2058  eqeq12i  2113  vtocl2  2696  spc2ev  2736  sbc2ie  2932  csbieb  2991  sseq12i  3075  uneq12i  3175  ineq12i  3222  nelpri  3498  ralpr  3525  rexpr  3526  preq12i  3552  dfop  3651  opeq12i  3657  breq12i  3884  mpteq2ia  3954  exmidundif  4067  exmidundifim  4068  opex  4089  opi2  4093  opth2  4100  opeqsn  4112  opeqpr  4113  uniop  4115  opelopaba  4126  braba  4127  opelopab  4131  brab  4132  opelopabaf  4133  unex  4300  snnex  4307  op1stb  4337  onun2i  4345  onsucssi  4360  ontr2exmid  4378  onsucsssucexmid  4380  onsucelsucexmid  4383  opthreg  4409  tfis  4435  finds  4452  finds2  4453  nnregexmid  4472  xpeq12i  4499  opelvv  4527  eqrelriiv  4571  eqrelrdv  4573  xpss  4585  xpex  4592  relop  4627  brco  4648  opelcnv  4659  brcnv  4660  asymref  4860  codir  4863  ssrnres  4917  dmprop  4949  dfco2  4974  cossxp  4997  cocnvss  5000  coex  5020  funsn  5107  fnsn  5113  feq23i  5203  resasplitss  5238  fabex  5247  fvex  5373  xpsn  5528  fmptap  5542  opabex  5576  acexmidlemv  5704  oveq12i  5718  oprabid  5735  oprabss  5789  caovcom  5860  opabex3  5951  iunex  5952  oprabex  5957  ofmres  5965  op1st  5975  op2nd  5976  fo1st  5986  fo2nd  5987  mpoex  6041  1stconst  6048  2ndconst  6049  algrflem  6056  dftpos4  6090  tpostpos  6091  tpossym  6103  frecex  6221  frecfnom  6228  sucinc  6271  fnoei  6278  oeiexg  6279  nnacli  6308  nnmcli  6309  elec  6398  ecovcom  6466  ecovass  6468  ecovdi  6470  fnmap  6479  mapval  6484  elmap  6501  elpm  6503  elpm2  6504  map0  6513  ixpconst  6532  entri  6610  endisj  6647  xpcomco  6649  phplem2  6676  ssfiexmid  6699  domfiexmid  6701  unfiexmid  6735  unfiin  6743  inresflem  6860  casefun  6885  caserel  6887  caseinj  6889  omp1eomlem  6894  omp1eom  6895  endjusym  6896  djufun  6904  djuinj  6906  ctssdclemr  6911  fodjuomnilemdc  6928  ctssexmid  6936  dju1p1e2  6962  exmidfodomrlemr  6967  exmidfodomrlemrALT  6968  1lt2pi  7049  indpi  7051  1nq  7075  rec1nq  7104  1lt2nq  7115  ltaddnq  7116  halfnqq  7119  prarloclemarch2  7128  prarloclemlt  7202  prarloclemcalc  7211  genpelxp  7220  ltexprlempr  7317  recexprlempr  7341  cauappcvgprlemcl  7362  cauappcvgprlemladd  7367  caucvgprlemcl  7385  caucvgprprlemcl  7413  0r  7446  1sr  7447  m1r  7448  m1p1sr  7456  m1m1sr  7457  0lt1sr  7461  1ne0sr  7462  1idsr  7464  recexgt0sr  7469  prsradd  7481  caucvgsrlemoffres  7495  caucvgsr  7497  pitonnlem1p1  7533  pitonnlem2  7534  pitoregt0  7536  peano2nnnn  7540  axi2m1  7560  axprecex  7565  axcnre  7566  nnindnn  7578  nntopi  7579  0cn  7630  addcli  7642  mulcli  7643  mulcomi  7644  readdcli  7651  remulcli  7652  rexpssxrxp  7682  ltrelxr  7697  gtneii  7730  lttri3i  7732  letri3i  7733  ltnsymi  7734  lenlti  7735  ltlei  7736  mulgt0i  7744  mulgt0ii  7745  0lt1  7760  addcomi  7777  pncan3oi  7849  resubcli  7896  subcli  7909  pncan3i  7910  negsubi  7911  subnegi  7912  subeq0i  7913  neg11i  7914  negcon1i  7915  negcon2i  7916  mulneg1i  8033  mulneg2i  8034  mul2negi  8035  addgt0ii  8120  ltnegi  8122  lenegi  8123  ltnegcon2i  8124  lesub0i  8125  ltaddposi  8126  posdifi  8127  ltnegcon1i  8128  lenegcon1i  8129  subge0i  8130  1ap0  8218  ltapii  8262  recrecapi  8365  dividapi  8366  div0api  8367  rec11apii  8382  divdiv32api  8388  recgt0ii  8523  ltrecii  8534  ltdiv23ii  8543  sup3exmid  8573  nnssre  8582  nnind  8594  nnmulcli  8600  nnsubi  8618  0le2  8668  1lt3  8743  2lt4  8745  1lt4  8746  3lt5  8748  2lt5  8749  1lt5  8750  4lt6  8752  3lt6  8753  2lt6  8754  1lt6  8755  5lt7  8757  4lt7  8758  3lt7  8759  2lt7  8760  1lt7  8761  6lt8  8763  5lt8  8764  4lt8  8765  3lt8  8766  2lt8  8767  1lt8  8768  7lt9  8770  6lt9  8771  5lt9  8772  4lt9  8773  3lt9  8774  2lt9  8775  1lt9  8776  2muline0  8797  nn0addcli  8866  nn0mulcli  8867  nn0addge1i  8877  nn0addge2i  8878  dfz2  8975  halfnz  8999  9p1e10  9036  numnncl  9043  numltc  9059  le9lt10  9060  nummac  9078  8lt10  9165  7lt10  9166  6lt10  9167  5lt10  9168  4lt10  9169  3lt10  9170  2lt10  9171  1lt10  9172  eluzaddi  9202  eluzsubi  9203  eluz2nn  9214  uzuzle23  9216  eluzge3nn  9217  divfnzn  9263  elq  9264  qreccl  9284  xrltnr  9407  mnfltpnf  9412  xaddmnf1  9472  pnfaddmnf  9474  mnfaddpnf  9475  xrex  9480  xaddid1  9486  xsubge0  9505  xposdif  9506  xleaddadd  9511  elicc2i  9563  ioomax  9572  iccmax  9573  ioopos  9574  elxrge0  9602  iccshftri  9619  iccshftli  9621  iccdili  9623  icccntri  9625  unitssre  9629  fz10  9667  fzpreddisj  9692  fldiv4p1lem1div2  9919  frecfzennn  10040  fnn0nninf  10051  fxnn0nninf  10052  0tonninf  10053  1tonninf  10054  m1expcl2  10156  m1expcl  10157  nn0expcli  10160  sqmuli  10216  cu2  10232  i3  10235  subsqi  10243  binom2subi  10248  bcpasc  10353  4bc2eq6  10361  hashinfom  10365  prhash2ex  10396  hashp1i  10397  rei  10512  imi  10513  readdi  10541  imaddi  10542  remuli  10543  immuli  10544  cjaddi  10545  cjmuli  10546  ipcni  10547  crrei  10549  crimi  10550  rexfiuz  10601  sqrt1  10658  sqrt4  10659  sqrt9  10660  abs1  10684  sqrtmulii  10746  abslti  10750  abslei  10751  abssubi  10762  absmuli  10763  sqabsaddi  10764  sqabssubi  10765  abstrii  10767  fimaxre2  10837  climz  10900  abscn2  10923  recn2  10925  imcn2  10926  climabs  10928  climre  10930  climim  10931  fsumcnv  11045  fsumrelem  11079  fsumre  11080  fsumim  11081  arisum2  11107  expcnv  11112  geo2sum2  11123  geo2lim  11124  0.999...  11129  geoihalfsum  11130  ege2le3  11175  ef0  11176  reeff1  11205  tan0  11236  ef01bndlem  11261  sin01bnd  11262  cos01bnd  11263  cos1bnd  11264  cos2bnd  11265  sin01gt0  11266  cos01gt0  11267  sin02gt0  11268  sincos1sgn  11269  sincos2sgn  11270  egt2lt3  11281  epos  11282  ene1  11286  eap1  11287  3dvdsdec  11357  3dvds2dec  11358  odd2np1lem  11364  n2dvds1  11404  z4even  11408  ndvdsi  11425  flodddiv4  11426  gcd0val  11444  6gcd4e2  11476  3lcm2e6woprm  11560  6lcm4e12  11561  3lcm2e6  11631  sqrt2irrlem  11632  phimullem  11693  xpnnen  11699  xpomen  11700  ennnfonelemj0  11706  ennnfonelem0  11710  ennnfonelemhf1o  11718  exmidunben  11731  qnnen  11736  setscom  11781  strleun  11830  txtopi  12211  txunii  12214  upxp  12222  uptx  12224  cnmpt1st  12238  cnmpt2nd  12239  qtopbasss  12443  cnmet  12452  remet  12459  blssioo  12464  tgqioo  12466  tgioo2cntop  12468  abscncf  12485  recncf  12486  imcncf  12487  cjcncf  12488  mulc1cncf  12489  cncfcn1cntop  12494  cdivcncfap  12499  expcncf  12504  ex-fl  12540  ex-ceil  12541  ex-bc  12544  ex-dvds  12545  ex-gcd  12546  bj-unex  12698  bj-nn0suc0  12733  bj-nntrans  12734  bj-nnelirr  12736  pw1dom2  12775  pwle2  12779  nnsf  12783  peano3nninf  12785  nninfex  12789  exmidsbthrlem  12801  sbthom  12805  isomninnlem  12809  trilpolemisumle  12815  trilpolemeq1  12817  trilpolemlt1  12818