Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > 3adant1r | Unicode version |
Description: Deduction adding a conjunct to antecedent. (Contributed by NM, 8-Jan-2006.) |
Ref | Expression |
---|---|
3adant1l.1 |
Ref | Expression |
---|---|
3adant1r |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 3adant1l.1 | . . . 4 | |
2 | 1 | 3expb 1199 | . . 3 |
3 | 2 | adantlr 474 | . 2 |
4 | 3 | 3impb 1194 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 wa 103 w3a 973 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 |
This theorem depends on definitions: df-bi 116 df-3an 975 |
This theorem is referenced by: 3adant2r 1228 3adant3r 1230 tfr1onlembacc 6321 tfr1onlembfn 6323 tfr1onlemaccex 6327 tfr1onlemres 6328 tfrcllembfn 6336 tfrcllemaccex 6340 tfrcllemres 6341 tfrcldm 6342 tfrcl 6343 mulassnqg 7346 prarloc 7465 prmuloc 7528 addasssrg 7718 axaddass 7834 |
Copyright terms: Public domain | W3C validator |