Mathbox for Jarvin Udandy < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  aibnbna Unicode version

Theorem aibnbna 27874
 Description: Given a implies b, not b, there exists a proof for not a. (Contributed by Jarvin Udandy, 1-Sep-2016.)
Hypotheses
Ref Expression
aibnbna.1
aibnbna.2
Assertion
Ref Expression
aibnbna

Proof of Theorem aibnbna
StepHypRef Expression
1 aibnbna.1 . . . . 5
2 ax-1 5 . . . . . . 7
3 aibnbna.2 . . . . . . . 8
43, 2mp1i 11 . . . . . . 7
52, 4ax-mp 8 . . . . . 6
6 ax-3 7 . . . . . 6
75, 6ax-mp 8 . . . . 5
81, 7pm3.2i 441 . . . 4
9 dfbi2 609 . . . . . 6
10 bicom 191 . . . . . . 7
1110biimpi 186 . . . . . 6
129, 11ax-mp 8 . . . . 5
1312biimpi 186 . . . 4
148, 13ax-mp 8 . . 3
15 nbfal 1316 . . . . 5
1615biimpi 186 . . . 4
173, 16mp1i 11 . . . 4
1816, 17ax-mp 8 . . 3
1914, 18aisbbisfaisf 27870 . 2
2019aisfina 27866 1
 Colors of variables: wff set class Syntax hints:   wn 3   wi 4   wb 176   wa 358   wfal 1308 This theorem is referenced by:  aibnbaif  27875 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8 This theorem depends on definitions:  df-bi 177  df-an 360  df-tru 1310  df-fal 1311
 Copyright terms: Public domain W3C validator