Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > 3adant3r | Unicode version |
Description: Deduction adding a conjunct to antecedent. (Contributed by NM, 8-Jan-2006.) |
Ref | Expression |
---|---|
3adant1l.1 |
Ref | Expression |
---|---|
3adant3r |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 3adant1l.1 | . . . 4 | |
2 | 1 | 3com13 1197 | . . 3 |
3 | 2 | 3adant1r 1220 | . 2 |
4 | 3 | 3com13 1197 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 wa 103 w3a 967 |
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 969 |
This theorem is referenced by: addassnqg 7314 mulassnqg 7316 prarloc 7435 ltpopr 7527 ltexprlemfl 7541 ltexprlemfu 7543 addasssrg 7688 axaddass 7804 apmul1 8675 ltmul2 8742 lemul2 8743 dvdscmulr 11746 dvdsmulcr 11747 modremain 11851 ndvdsadd 11853 rpexp12i 12064 xblcntrps 12954 xblcntr 12955 |
Copyright terms: Public domain | W3C validator |