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  1326  barbara  2111  eqeq12i  2178  vtocl2  2776  spc2ev  2817  sbc2ie  3017  csbieb  3081  sseq12i  3165  uneq12i  3269  ineq12i  3316  ifssun  3529  nelpri  3594  ralpr  3625  rexpr  3626  preq12i  3652  dfop  3751  opeq12i  3757  breq12i  3985  mpteq2ia  4062  exmidundif  4179  exmidundifim  4180  opex  4201  opi2  4205  opth2  4212  opeqsn  4224  opeqpr  4225  uniop  4227  opelopaba  4238  braba  4239  opelopab  4243  brab  4244  opelopabaf  4245  unex  4413  snnex  4420  op1stb  4450  ifelpwun  4455  onun2i  4462  onsucssi  4477  ontriexmidim  4493  ontr2exmid  4496  onsucsssucexmid  4498  onsucelsucexmid  4501  opthreg  4527  tfis  4554  finds  4571  finds2  4572  nnregexmid  4592  xpeq12i  4620  opelvv  4648  eqrelriiv  4692  eqrelrdv  4694  xpss  4706  xpex  4713  relop  4748  brco  4769  opelcnv  4780  brcnv  4781  asymref  4983  codir  4986  ssrnres  5040  dmprop  5072  dfco2  5097  cossxp  5120  cocnvss  5123  coex  5143  funsn  5230  fnsn  5236  feq23i  5326  resasplitss  5361  fabex  5370  fvex  5500  xpsn  5655  fmptap  5669  opabex  5703  acexmidlemv  5834  oveq12i  5848  oprabid  5865  oprabss  5919  caovcom  5990  opabex3  6082  iunex  6083  oprabex  6088  ofmres  6096  op1st  6106  op2nd  6107  fo1st  6117  fo2nd  6118  mpoex  6173  1stconst  6180  2ndconst  6181  algrflem  6188  dftpos4  6222  tpostpos  6223  tpossym  6235  frecex  6353  frecfnom  6360  sucinc  6404  fnoei  6411  oeiexg  6412  nnacli  6441  nnmcli  6442  elec  6531  ecovcom  6599  ecovass  6601  ecovdi  6603  fnmap  6612  mapval  6617  elmap  6634  elpm  6636  elpm2  6637  map0  6646  ixpconst  6665  entri  6743  endisj  6781  xpcomco  6783  phplem2  6810  ssfiexmid  6833  domfiexmid  6835  unfiexmid  6874  unfiin  6882  inresflem  7016  casefun  7041  caserel  7043  caseinj  7045  omp1eomlem  7050  omp1eom  7051  endjusym  7052  djufun  7060  djuinj  7062  ctssdccl  7067  ctssdclemr  7068  nninfex  7077  infnninf  7079  fodjuomnilemdc  7099  ctssexmid  7105  exmidonfinlem  7140  dju1p1e2  7144  exmidfodomrlemr  7149  exmidfodomrlemrALT  7150  exmidaclem  7155  pw1dom2  7174  onntri35  7184  onntri45  7188  1lt2pi  7272  indpi  7274  1nq  7298  rec1nq  7327  1lt2nq  7338  ltaddnq  7339  halfnqq  7342  prarloclemarch2  7351  prarloclemlt  7425  prarloclemcalc  7434  genpelxp  7443  ltexprlempr  7540  recexprlempr  7564  cauappcvgprlemcl  7585  cauappcvgprlemladd  7590  caucvgprlemcl  7608  caucvgprprlemcl  7636  suplocexprlemell  7645  suplocexprlemdisj  7652  suplocexprlemub  7655  0r  7682  1sr  7683  m1r  7684  m1p1sr  7692  m1m1sr  7693  0lt1sr  7697  1ne0sr  7698  1idsr  7700  recexgt0sr  7705  prsradd  7718  caucvgsrlemoffres  7732  caucvgsr  7734  mappsrprg  7736  map2psrprg  7737  pitonnlem1p1  7778  pitonnlem2  7779  pitoregt0  7781  peano2nnnn  7785  axi2m1  7807  axprecex  7812  axcnre  7813  nnindnn  7825  nntopi  7826  0cn  7882  addcli  7894  mulcli  7895  mulcomi  7896  readdcli  7903  remulcli  7904  rexpssxrxp  7934  ltrelxr  7950  gtneii  7985  lttri3i  7987  letri3i  7988  ltnsymi  7989  lenlti  7990  ltlei  7991  mulgt0i  7999  mulgt0ii  8000  0lt1  8016  addcomi  8033  pncan3oi  8105  resubcli  8152  subcli  8165  pncan3i  8166  negsubi  8167  subnegi  8168  subeq0i  8169  neg11i  8170  negcon1i  8171  negcon2i  8172  mulneg1i  8293  mulneg2i  8294  mul2negi  8295  addgt0ii  8380  ltnegi  8382  lenegi  8383  ltnegcon2i  8384  lesub0i  8385  ltaddposi  8386  posdifi  8387  ltnegcon1i  8388  lenegcon1i  8389  subge0i  8390  1ap0  8479  ltapii  8524  recrecapi  8631  dividapi  8632  div0api  8633  rec11apii  8648  divdiv32api  8654  recgt0ii  8793  ltrecii  8804  ltdiv23ii  8813  sup3exmid  8843  nnssre  8852  nnind  8864  nnmulcli  8870  nnsubi  8888  0le2  8938  1lt3  9019  2lt4  9021  1lt4  9022  3lt5  9024  2lt5  9025  1lt5  9026  4lt6  9028  3lt6  9029  2lt6  9030  1lt6  9031  5lt7  9033  4lt7  9034  3lt7  9035  2lt7  9036  1lt7  9037  6lt8  9039  5lt8  9040  4lt8  9041  3lt8  9042  2lt8  9043  1lt8  9044  7lt9  9046  6lt9  9047  5lt9  9048  4lt9  9049  3lt9  9050  2lt9  9051  1lt9  9052  2muline0  9073  nn0addcli  9142  nn0mulcli  9143  nn0addge1i  9153  nn0addge2i  9154  dfz2  9254  halfnz  9278  9p1e10  9315  numnncl  9322  numltc  9338  le9lt10  9339  nummac  9357  8lt10  9444  7lt10  9445  6lt10  9446  5lt10  9447  4lt10  9448  3lt10  9449  2lt10  9450  1lt10  9451  eluzaddi  9483  eluzsubi  9484  eluz2nn  9495  eluz4eluz2  9496  uzuzle23  9500  eluzge3nn  9501  divfnzn  9550  elq  9551  qreccl  9571  xrltnr  9706  mnfltpnf  9712  xaddmnf1  9775  pnfaddmnf  9777  mnfaddpnf  9778  xrex  9783  xaddid1  9789  xsubge0  9808  xposdif  9809  xleaddadd  9814  elicc2i  9866  ioomax  9875  iccmax  9876  ioopos  9877  elxrge0  9905  iccshftri  9922  iccshftli  9924  iccdili  9926  icccntri  9928  unitssre  9932  fz10  9971  fzpreddisj  9996  fz0to4untppr  10049  dfrp2  10189  fldiv4p1lem1div2  10230  frecfzennn  10351  fnn0nninf  10362  fxnn0nninf  10363  0tonninf  10364  1tonninf  10365  m1expcl2  10467  m1expcl  10468  nn0expcli  10471  sqmuli  10527  cu2  10543  i3  10546  subsqi  10554  binom2subi  10559  bcpasc  10668  4bc2eq6  10676  hashinfom  10680  prhash2ex  10711  hashp1i  10712  rei  10827  imi  10828  readdi  10856  imaddi  10857  remuli  10858  immuli  10859  cjaddi  10860  cjmuli  10861  ipcni  10862  crrei  10864  crimi  10865  rexfiuz  10917  sqrt1  10974  sqrt4  10975  sqrt9  10976  abs1  11000  sqrtmulii  11062  abslti  11066  abslei  11067  abssubi  11078  absmuli  11079  sqabsaddi  11080  sqabssubi  11081  abstrii  11083  fimaxre2  11154  climz  11219  abscn2  11242  recn2  11244  imcn2  11245  climabs  11247  climre  11249  climim  11250  fsumcnv  11364  fsumrelem  11398  fsumre  11399  fsumim  11400  arisum2  11426  expcnv  11431  geo2sum2  11442  geo2lim  11443  0.999...  11448  geoihalfsum  11449  fprodcnv  11552  fprodge0  11564  fprodge1  11566  ege2le3  11598  ef0  11599  reeff1  11627  tan0  11658  ef01bndlem  11683  sin01bnd  11684  cos01bnd  11685  cos1bnd  11686  cos2bnd  11687  sin01gt0  11688  cos01gt0  11689  sin02gt0  11690  sincos1sgn  11691  sincos2sgn  11692  cos12dec  11694  egt2lt3  11706  epos  11707  ene1  11711  eap1  11712  3dvdsdec  11787  3dvds2dec  11788  odd2np1lem  11794  n2dvds1  11834  z4even  11838  ndvdsi  11855  flodddiv4  11856  gcd0val  11878  6gcd4e2  11913  3lcm2e6woprm  11997  6lcm4e12  11998  3lcm2e6  12069  sqrt2irrlem  12070  phimullem  12134  xpnnen  12264  xpomen  12265  ennnfonelemj0  12271  ennnfonelem0  12275  ennnfonelemhf1o  12283  exmidunben  12296  qnnen  12301  unct  12312  setscom  12371  strleun  12420  txtopi  12802  txunii  12805  upxp  12813  uptx  12815  cnmpt1st  12829  cnmpt2nd  12830  txswaphmeolem  12861  qtopbasss  13062  cnmet  13071  cnopncntop  13078  remet  13081  blssioo  13086  tgqioo  13088  tgioo2cntop  13090  divcnap  13096  abscncf  13113  recncf  13114  imcncf  13115  cjcncf  13116  mulc1cncf  13117  cncfcn1cntop  13122  cdivcncfap  13128  expcncf  13133  cnrehmeocntop  13134  limccnp2lem  13186  limccnp2cntop  13187  dvcnp2cntop  13204  dvaddxxbr  13206  dvmulxxbr  13207  dvcoapbr  13212  dvrecap  13218  dveflem  13228  dvef  13229  sincn  13231  coscn  13232  reeff1oleme  13234  reeff1o  13235  cosz12  13242  sin0pilem1  13243  sin0pilem2  13244  pipos  13250  sinhalfpilem  13253  sincosq1lem  13287  sincosq1sgn  13288  sincosq2sgn  13289  sincosq3sgn  13290  sincosq4sgn  13291  sinq12gt0  13292  cosq14gt0  13294  cosq23lt0  13295  coseq0q4123  13296  coseq00topi  13297  coseq0negpitopi  13298  tangtx  13300  sincos4thpi  13302  tan4thpi  13303  sincos6thpi  13304  pigt3  13306  cosordlem  13311  cosq34lt1  13312  cos02pilt1  13313  cos0pilt1  13314  ioocosf1o  13316  negpitopissre  13317  log1  13328  loge  13329  2logb9irr  13430  sqrt2cxp2logb9e3  13434  2logb9irrap  13436  ex-fl  13443  ex-ceil  13444  ex-bc  13447  ex-dvds  13448  ex-gcd  13449  bj-charfunbi  13528  bj-unex  13636  bj-nn0suc0  13667  bj-nntrans  13668  bj-nnelirr  13670  012of  13709  2o01f  13710  pwle2  13712  nnsf  13719  peano3nninf  13721  exmidsbthrlem  13735  sbthom  13739  isomninnlem  13743  iooref1o  13747  trilpolemisumle  13751  trilpolemeq1  13753  trilpolemlt1  13754  apdiff  13761  iswomninnlem  13762  iswomni0  13764  ismkvnnlem  13765  dceqnconst  13772  dcapnconst  13773  nconstwlpolemgt0  13776  taupi  13783