Theorem mp2an 416

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

Syntax hints:   → wi 4   ∧ wa 102

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

This theorem is referenced by:  mp4an  417  jaoi  668  mp3an  1268  barbara  2039  eqeq12i  2094  vtocl2  2654  spc2ev  2693  sbc2ie  2885  csbieb  2944  sseq12i  3025  uneq12i  3124  ineq12i  3165  nelpri  3422  ralpr  3447  rexpr  3448  preq12i  3474  dfop  3569  opeq12i  3575  breq12i  3794  mpteq2ia  3864  opex  3984  opi2  3988  opth2  3995  opeqsn  4007  opeqpr  4008  uniop  4010  opelopaba  4021  braba  4022  opelopab  4026  brab  4027  opelopabaf  4028  unex  4194  snnex  4199  op1stb  4227  onun2i  4235  onsucssi  4250  ontr2exmid  4268  onsucsssucexmid  4270  onsucelsucexmid  4273  opthreg  4299  tfis  4324  finds  4341  finds2  4342  nnregexmid  4360  xpeq12i  4385  opelvv  4408  eqrelriiv  4452  eqrelrdv  4454  xpss  4464  xpex  4471  relop  4504  brco  4524  opelcnv  4535  brcnv  4536  asymref  4730  codir  4733  ssrnres  4783  dmprop  4815  dfco2  4840  cossxp  4863  coex  4883  funsn  4968  fnsn  4973  feq23i  5061  resasplitss  5089  fabex  5098  fvex  5215  xpsn  5360  fmptap  5374  opabex  5406  acexmidlemv  5530  oveq12i  5544  oprabid  5557  oprabss  5610  caovcom  5678  opabex3  5769  iunex  5770  oprabex  5775  ofmres  5783  op1st  5793  op2nd  5794  fo1st  5804  fo2nd  5805  mpt2ex  5856  1stconst  5862  2ndconst  5863  algrflem  5870  dftpos4  5901  tpostpos  5902  tpossym  5914  frecex  6004  frecfnom  6009  sucinc  6048  fnoei  6055  oeiexg  6056  nnacli  6084  nnmcli  6085  elec  6168  ecovcom  6236  ecovass  6238  ecovdi  6240  entri  6289  endisj  6321  xpcomco  6323  phplem2  6339  ssfiexmid  6361  domfiexmid  6363  1lt2pi  6530  indpi  6532  1nq  6556  rec1nq  6585  1lt2nq  6596  ltaddnq  6597  halfnqq  6600  prarloclemarch2  6609  prarloclemlt  6683  prarloclemcalc  6692  genpelxp  6701  ltexprlempr  6798  recexprlempr  6822  cauappcvgprlemcl  6843  cauappcvgprlemladd  6848  caucvgprlemcl  6866  caucvgprprlemcl  6894  0r  6927  1sr  6928  m1r  6929  m1p1sr  6937  m1m1sr  6938  0lt1sr  6942  1ne0sr  6943  1idsr  6945  recexgt0sr  6950  prsradd  6962  caucvgsrlemoffres  6976  caucvgsr  6978  pitonnlem1p1  7014  pitonnlem2  7015  pitoregt0  7017  peano2nnnn  7021  axi2m1  7041  axprecex  7046  axcnre  7047  nnindnn  7059  nntopi  7060  0cn  7111  addcli  7123  mulcli  7124  mulcomi  7125  readdcli  7132  remulcli  7133  rexpssxrxp  7163  ltrelxr  7173  gtneii  7206  lttri3i  7208  letri3i  7209  ltnsymi  7210  lenlti  7211  ltlei  7212  mulgt0i  7220  mulgt0ii  7221  0lt1  7236  addcomi  7252  pncan3oi  7324  resubcli  7371  subcli  7384  pncan3i  7385  negsubi  7386  subnegi  7387  subeq0i  7388  neg11i  7389  negcon1i  7390  negcon2i  7391  mulneg1i  7508  mulneg2i  7509  mul2negi  7510  addgt0ii  7592  ltnegi  7594  lenegi  7595  ltnegcon2i  7596  lesub0i  7597  ltaddposi  7598  posdifi  7599  ltnegcon1i  7600  lenegcon1i  7601  subge0i  7602  1ap0  7690  ltapii  7733  recrecapi  7832  dividapi  7833  div0api  7834  rec11apii  7849  divdiv32api  7855  recgt0ii  7985  ltrecii  7996  ltdiv23ii  8005  nnssre  8043  nnind  8055  nnmulcli  8061  nnsubi  8078  0le2  8129  1lt3  8203  2lt4  8205  1lt4  8206  3lt5  8208  2lt5  8209  1lt5  8210  4lt6  8212  3lt6  8213  2lt6  8214  1lt6  8215  5lt7  8217  4lt7  8218  3lt7  8219  2lt7  8220  1lt7  8221  6lt8  8223  5lt8  8224  4lt8  8225  3lt8  8226  2lt8  8227  1lt8  8228  7lt9  8230  6lt9  8231  5lt9  8232  4lt9  8233  3lt9  8234  2lt9  8235  1lt9  8236  2muline0  8256  nn0addcli  8325  nn0mulcli  8326  nn0addge1i  8336  nn0addge2i  8337  dfz2  8420  halfnz  8443  9p1e10  8479  numnncl  8486  numltc  8502  le9lt10  8503  nummac  8521  8lt10  8608  7lt10  8609  6lt10  8610  5lt10  8611  4lt10  8612  3lt10  8613  2lt10  8614  1lt10  8615  eluzaddi  8645  eluzsubi  8646  eluz2nn  8657  uzuzle23  8659  eluzge3nn  8660  divfnzn  8706  elq  8707  qreccl  8727  xrltnr  8855  mnfltpnf  8860  xrex  8910  elicc2i  8962  ioomax  8971  iccmax  8972  ioopos  8973  elxrge0  9001  iccshftri  9017  iccshftli  9019  iccdili  9021  icccntri  9023  unitssre  9027  fz10  9065  fzpreddisj  9088  fldiv4p1lem1div2  9307  frecfzennn  9419  m1expcl2  9498  m1expcl  9499  nn0expcli  9502  sqmuli  9558  cu2  9573  i3  9576  subsqi  9584  binom2subi  9588  bcpasc  9693  4bc2eq6  9701  rei  9786  imi  9787  readdi  9815  imaddi  9816  remuli  9817  immuli  9818  cjaddi  9819  cjmuli  9820  ipcni  9821  crrei  9823  crimi  9824  rexfiuz  9875  sqrt1  9932  sqrt4  9933  sqrt9  9934  abs1  9958  sqrtmulii  10020  abslti  10024  abslei  10025  abssubi  10036  absmuli  10037  sqabsaddi  10038  sqabssubi  10039  abstrii  10041  fimaxre2  10109  climz  10131  abscn2  10153  recn2  10155  imcn2  10156  climabs  10158  climre  10160  climim  10161  3dvdsdec  10264  3dvds2dec  10265  odd2np1lem  10271  n2dvds1  10312  z4even  10316  ndvdsi  10333  flodddiv4  10334  gcd0val  10352  6gcd4e2  10384  eucialg  10441  3lcm2e6woprm  10468  6lcm4e12  10469  3lcm2e6  10539  sqrt2irrlem  10540  ex-fl  10563  ex-ceil  10564  ex-bc  10566  ex-dvds  10567  ex-gcd  10568  bj-unex  10710  bj-nn0suc0  10745  bj-nntrans  10746  bj-nnelirr  10748