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

Theorem pm2.21i 123
Description: A contradiction implies anything. Inference from pm2.21 100. (Contributed by NM, 16-Sep-1993.)
Hypothesis
Ref Expression
pm2.21i.1 ¬ φ
Assertion
Ref Expression
pm2.21i (φψ)

Proof of Theorem pm2.21i
StepHypRef Expression
1 pm2.21i.1 . . 3 ¬ φ
21a1i 10 . 2 ψ → ¬ φ)
32con4i 122 1 (φψ)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem is referenced by:  pm2.24ii  124  pm3.2ni  827  falim  1328  nfnth  1556  ax4sp1  2174  rex0  3563  0ss  3579  abf  3584  r19.2zb  3640  ral0  3654  snsssn  3873  int0  3940  clos10  5887  po0  5939  connex0  5940  fnfreclem2  6318  fnfreclem3  6319
  Copyright terms: Public domain W3C validator