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

Theorem pm2.61i 156
Description: Inference eliminating an antecedent. (Contributed by NM, 5-Apr-1994.) (Proof shortened by Wolf Lammen, 12-Sep-2013.)
Hypotheses
Ref Expression
pm2.61i.1
pm2.61i.2
Assertion
Ref Expression
pm2.61i

Proof of Theorem pm2.61i
StepHypRef Expression
1 id 19 . 2
2 pm2.61i.2 . . 3
3 pm2.61i.1 . . 3
42, 3ja 153 . 2
51, 4ax-mp 5 1
Colors of variables: wff setvar class
Syntax hints:   wn 3   wi 4
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem is referenced by:  pm2.61ii  157  pm2.61nii  158  pm2.61iii  159  pm2.65i  165  pm5.21nii  342  pm5.18  345  biass  348  pm2.61ian  765  ecase3  907  4cases  915  elimh  922  pm4.42  926  3ecase  1286  ax9  1949  dvelimh  1964  exdistrf  1971  equveli  1988  dfsb2  2055  sbn  2062  sbi1  2063  sbco2  2086  sbco3  2088  sb9i  2094  ax11v  2096  hbs1  2105  nfsb  2109  sbal1  2126  sbal  2127  dvelimALT  2133  ax11  2155  equid1  2158  equid1ALT  2176  dvelimf-o  2180  ax11inda2ALT  2198  ax11inda2  2199  eujustALT  2207  moexex  2273  pm2.61ne  2591  pm2.61ine  2592  rgen2a  2680  ralcom2  2775  eueq2  3010  moeq3  3013  mo2icl  3015  sbc2or  3054  unineq  3505  ralidm  3653  ifsb  3671  ifid  3694  ifnot  3700  ifan  3701  ifor  3702  elimhyp  3710  elimhyp2v  3711  elimhyp3v  3712  elimhyp4v  3713  elimdhyp  3715  keephyp2v  3717  keephyp3v  3718  ssunsn2  3865  snex  4111  setswith  4321  iotassuni  4355  iotaex  4356  dfiota3  4370  dfiota4  4372  snfi  4431  eqtfinrelk  4486  dfphi2  4569  copsexg  4607  phiall  4618  dfid3  4768  imasn  5018  dmsnopss  5067  fveqres  5355  eqfnfv  5392  f0cli  5418  fvunsn  5444  fconst5  5455  elimdelov  5573  ndmovcl  5614  ndmovord  5620  fvmptss  5705  fvmptex  5721  fvmptss2  5725  fvfullfun  5864  nchoicelem12  6300  frecxp  6314
  Copyright terms: Public domain W3C validator