Theorem mp2an 653

Description: An inference based on modus ponens. (Contributed by NM, 13-Apr-1995.)

Hypotheses

Ref	Expression
mp2an.1	|- ph
mp2an.2	|- ps
mp2an.3	|- ((ph /\ ps) -> ch)

Assertion

Ref	Expression
mp2an	|- ch

Proof of Theorem mp2an

Step	Hyp	Ref	Expression
1		mp2an.2	. 2 |- ps
2		mp2an.1	. . 3 |- ph
3		mp2an.3	. . 3 |- ((ph /\ ps) -> ch)
4	2, 3	mpan 651	. 2 |- (ps -> ch)
5	1, 4	ax-mp 5	1 |- ch

Syntax hints:   -> wi 4   /\ wa 358

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

This theorem depends on definitions:  df-bi 177  df-an 360

This theorem is referenced by:  mp4an  654  mp3an  1277  nanbi12i  1300  cadtru  1401  spim  1975  barbara  2301  eqeq12i  2366  vtocl2  2911  spc2ev  2948  mosub  3015  sbc2ie  3114  csbieb  3175  nineq12i  3240  symdifeq12i  3254  sseq12i  3298  uneq12i  3417  ineq12i  3456  keephyp  3717  nelpri  3755  ralpr  3780  rexpr  3781  preq12i  3805  opkeq12i  4065  ninex  4099  inex  4106  unex  4107  difex  4108  symdifex  4109  pw111  4171  xpkeq12i  4204  eqrelkriiv  4214  eqrelkrdv  4215  opkelopkab  4247  opkelxpk  4249  opkelcnvk  4251  otkelins2kg  4254  otkelins3kg  4255  opkelcokg  4262  opkelcok  4263  opksnelsik  4266  sikss1c1c  4268  elssetk  4271  opkelimagek  4273  ins2kss  4280  ins3kss  4281  cokrelk  4285  cnvkexg  4287  xpkex  4290  ssetkex  4295  sikexlem  4296  imakex  4301  dfpw12  4302  insklem  4305  cokex  4311  dfidk2  4314  addceq12i  4389  addcex  4395  dfnnc2  4396  nnc0suc  4413  nncaddccl  4420  0fin  4424  nnsucelrlem1  4425  nnsucelr  4429  nndisjeq  4430  ltfinp1  4463  lefinlteq  4464  lefinrflx  4468  ssfin  4471  eqpwrelk  4479  ncfinraise  4482  ncfinlower  4484  eqtfinrelk  4487  tfin0c  4498  tfin1c  4500  tfinltfinlem1  4501  tfinltfin  4502  oddfinex  4505  0ceven  4506  evenodddisjlem1  4516  nnpweq  4524  srelk  4525  sfin01  4529  sfinltfin  4536  vfinspsslem1  4551  dfphi2  4570  opex  4589  breq12i  4649  opelopaba  4704  braba  4705  opelopab  4709  brab  4710  opelopabaf  4711  setconslem1  4732  dfsset2  4744  imaex  4748  coex  4751  dfsi2  4752  brsset  4759  xpeq12i  4807  dmprop  5071  xpex  5116  resex  5118  feq23i  5220  fvi  5443  swapres  5513  opfv1st  5515  opfv2nd  5516  oveq12i  5536  caovcom  5626  mpteq2ia  5660  txpex  5786  brcup  5816  composefn  5819  brdisj  5823  braddcfn  5827  pprodex  5839  brcross  5850  brpw1fn  5855  fnfullfun  5859  dfnnc3  5886  qsex  5984  mapval  6012  endisj  6052  xpassen  6058  ensn  6059  enmap2lem1  6064  enmap1lem1  6070  enpw1pw  6076  enpw  6088  brlec  6114  mucnc  6132  1cnc  6140  ncspw1eu  6160  tc0c  6164  tcdi  6165  tc1c  6166  tc2c  6167  ce0nnul  6178  ce0addcnnul  6180  ce0nn  6181  cenc  6182  fce  6189  ce2  6193  lecncvg  6200  nclenc  6223  taddc  6230  letc  6232  ce0t  6233  cet  6235  ce0lenc1  6240  brtcfn  6247  ncvsq  6257  nnltp1c  6263  nmembers1lem2  6270  nncdiv3  6278  nnc3n3p1  6279  nchoicelem9  6298  nchoicelem14  6303  nchoicelem17  6306  fnfreclem2  6319  fnfreclem3  6320