NFE Home New Foundations Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  NFE Home  >  Th. List  >  mpan2 Unicode version

Theorem mpan2 652
Description: An inference based on modus ponens. (Contributed by NM, 16-Sep-1993.) (Proof shortened by Wolf Lammen, 19-Nov-2012.)
Hypotheses
Ref Expression
mpan2.1
mpan2.2
Assertion
Ref Expression
mpan2

Proof of Theorem mpan2
StepHypRef Expression
1 mpan2.1 . . 3
21a1i 10 . 2
3 mpan2.2 . 2
42, 3mpdan 649 1
Colors of variables: wff setvar class
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:  mpanr12  666  mp3an23  1269  equs4  1959  eueq2  3010  sbcgf  3109  csbconstgf  3149  sbcnestg  3185  csbnestg  3186  csbnest1g  3188  eqpw1  4162  imakexg  4299  imagekexg  4311  setswith  4321  eqpw1uni  4330  sspw1  4335  finds  4411  nnc0suc  4412  elsuci  4414  lefinaddc  4450  nulge  4456  ltfinp1  4462  ncfinsn  4476  tfinltfinlem1  4500  sucevenodd  4510  sucoddeven  4511  oddtfin  4518  sfintfin  4532  vfinspnn  4541  1cvsfin  4542  tncveqnc1fin  4544  vfintle  4546  vfin1cltv  4547  vfinncvntnn  4548  vfinspsslem1  4550  vfinncsp  4554  vinf  4555  epelc  4765  xpss1  4856  br1st  4858  br2nd  4859  brswap2  4860  ssrnres  5059  rnexg  5104  resexg  5116  funcnvres  5165  fnresin1  5197  fnresin2  5198  fvopab3g  5386  fvopab4  5389  fsn  5432  fsn2  5434  f1elima  5474  mpteq1  5658  fvmpt  5700  fvmptnf  5723  fixexg  5788  ins3exg  5796  imageexg  5800  pprodexg  5837  clos1induct  5880  ecexg  5949  ecelqsg  5979  enmap2lem3  6065  enpw  6087  ncaddccl  6144  peano2nc  6145  ncdisjeq  6148  pw1eltc  6162  ovcelem1  6171  ce0nnul  6177  ce0nn  6180  ce0nulnc  6184  ce0  6190  lecidg  6196  lecncvg  6199  leconnnc  6218  ncfin  6247  nclenn  6249  ncslesuc  6267  nmembers1  6271  spaccl  6286  nchoicelem3  6291  nchoicelem9  6297  nchoicelem19  6307  frecxpg  6315  fnfreclem1  6317  fnfreclem3  6319  scancan  6331
  Copyright terms: Public domain W3C validator