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 1186 | . . 3 |
3 | 2 | adantlr 469 | . 2 |
4 | 3 | 3impb 1181 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 wa 103 w3a 963 |
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 965 |
This theorem is referenced by: 3adant2r 1215 3adant3r 1217 tfr1onlembacc 6286 tfr1onlembfn 6288 tfr1onlemaccex 6292 tfr1onlemres 6293 tfrcllembfn 6301 tfrcllemaccex 6305 tfrcllemres 6306 tfrcldm 6307 tfrcl 6308 mulassnqg 7299 prarloc 7418 prmuloc 7481 addasssrg 7671 axaddass 7787 |
Copyright terms: Public domain | W3C validator |