Theorem mp2an 520

Description: An inference based on modus ponens.

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 518	. 2 ⊢ (ψ → χ)
5	1, 4	ax-mp 6	1 ⊢ χ

Syntax hints:   → wi 2   ∧ wa 196

This theorem is referenced by:  mp3an 642  vtocl2 1379  cla4e2v 1406  mosub 1433  undir 1679  opthwiener 1914  iun0 2028  opelopab 2117  brab 2118  ideq 2127  tfis 2245  onssel 2357  onun 2358  onsucss 2359  finds 2397  finds2 2399  xp0r 2474  cleqreli 2484  opelcnv 2518  dm0 2542  dmsn0 2543  dmsnsn0 2544  intirr 2628  cnv0 2633  cores 2659  co02 2663  coexg 2671  coex 2672  fcoi1 2765  fcoi2 2766  fcnvres 2768  fvopabf 2876  fvi 2900  abrexexlem2 2911  tz7.48-2 2995  elxp6 3093  1st2val 3097  df1st2 3098  oawordeulem 3156  ecoprcom 3255  ecoprass 3256  ecoprdi 3257  fnmap 3262  mapval 3264  entr 3321  endisj 3341  xpen 3383  pwen 3398  0sdom1dom 3420  unfilem1 3438  prfi 3444  en2lp 3453  inf0 3457  inf4 3473  dfom3 3477  infensuc 3484  trcl 3489  rankr1 3518  rankel 3524  rankss 3531  rankpr 3536  ranklon 3540  scottex 3541  zornlem4 3606  cardon 3634  cardid 3635  carden 3638  cardsn 3640  carddom 3642  cardsdom 3643  domtri 3644  unxpdomlem 3649  unxpdom2 3651  sucxpdom 3652  cardprc 3667  aleph1 3676  alephord 3680  alephord3 3683  alephgeom 3687  cfom 3710  cdaval 3717  uncdadom 3718  cdaen 3719  cda1en 3721  cdacomen 3724  cdaassen 3725  xpcdaen 3726  cdadom1 3727  cdadom3 3729  cdainf 3731  1lt2pi 3826  1q 3851  mulidpq 3863  1lt2pq 3872  halfpq 3876  distrlem5pr 3925  prlem934b 3932  0r 3983  1r 3984  m1r 3985  m1p1sr 3995  m1m1sr 3996  0lt1sr 3998  1ne0sr 3999  1idsr 4001  recexsrlem 4006  mappsrpr 4012  axresscn 4062  axi2m1 4082  addcl 4104  mulcl 4105  addcom 4106  mulcom 4107  recex 4117  readdcl 4118  remulcl 4119  add4 4130  subval 4134  resubcl 4174  mul4 4180  muln0 4214  divval 4217  divneq0 4231  divmuldiv 4266  divadddiv 4268  divdivdiv 4269  redivcl 4274  lttri2 4295  lttri3 4296  letri3 4297  leloe 4298  ltlen 4299  ltnsym 4300  lelt 4301  ltle 4302  ltne 4305  addgt0i 4326  mulgt0 4334  mulgt0i 4336  recgt0i 4385  nnssre 4425  nnind 4434  0nnn 4443  2nn 4487  nn0addcl 4552  nn0mulcl 4553  nn0ltp1let 4556  nn0subt 4587  zltp1let 4597  uzind 4603  om2uzran 4655  uzrdgini 4658  seqval 4665  cu2 4711  nnsqcl 4717  nn0le2sqet 4721  nn0opthlem1 4722  nn0opth 4724  sqr0 4730  sqrlem1 4731  sqrlem2 4732  sqrlem6 4736  sqrlem8 4738  sqrlem13 4743  sqrlem24 4754  sqrgt0i 4755  sqrlem26 4756  sqrmuli 4762  sqr4 4772  sqr9 4773  sqr2irrlem1 4777  sqr2irrlem4 4780  nthruc 4784  nthruz 4785  cjmulge0 4823  abs00 4839  releabs 4858  abstri 4859  fac0 4871  clim0 4882  ruclem10 4894  ruclem11 4895  ruclem13 4897  ruclem15 4899  ruclem17 4901  ruclem22 4906  ruclem23 4907  ruclem24 4908  ruclem25 4909  ruclem26 4910  ruclem27 4911  ruclem28 4912  ruclem29 4913  ruclem30 4914  ruclem31 4915  ruclem32 4916  ruclem33 4917  ruclem35 4919  ruclem39 4923  xpnnen 4927  xpomen 4928  znnen 4930  qnnen 4931  resdomq 4932  infxpidmlem9 4941  infxpidmlem12 4944  infdif 4948  infmap1 4950  hvmulcl 4990  hvaddcl 4999  hvcom 5000  hvsubval 5001  hvsubcl 5002  hvadd4 5030  hicl 5044  normlem2 5064  normlem6 5068  normlem7 5069  bcseq 5073  norm-ii 5086  normpyth 5090  bcs 5101  hlim0 5140  hlimcaui 5141  shsspwh 5153  chsspwh 5154  occon2 5170  projlem2 5194  projlem3 5195  projlem4 5196  projlem5 5197  projlem6 5198  projlem8 5200  projlem13 5205  projlem14 5206  projlem15 5207  projlem18 5210  projlem28 5220  pjthlem1 5225  pjthlem5 5229  pjthlem6 5230  pjthlem13 5237  omlsilem 5249  pjpj0 5259  pjpj 5261  pjpjth 5263  pjop 5266  pjpo 5267  pjococ 5272  shsel 5281  shscl 5282  chjval 5324  shscom 5333  shsva 5334  shsel1 5335  shsel2 5336  shslej 5339  shjcom 5341  shjcl 5345  shlub 5347  shsumval2 5361  chsscon3 5383  chdmm1 5398  shjshs 5412  chabs1 5434  chabs2 5435  ledi 5447  span0 5448  spanun 5450  sshhococ 5451  chsup0 5453  h1de2 5458  spansnpj 5481  pjoml4 5497  cmbr 5499  5oa 5551  pjadj 5564  pjadd 5566  pjmul 5568  pjsslem 5570  pjdifnorm 5574  pjoi0 5592  hoeq 5595  hocof 5600  hosf 5602  hodf 5603  ho1 5613  pjnel 5665  hatomistic 5755  chpssat 5756  cvexchlem 5759  cvexch 5760  mdsymlem6 5781  mdsym 5784  sumdmdi 5785

This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-3 5  ax-mp 6

This theorem depends on definitions:  df-bi 128  df-an 198

metamath.org