Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > simpll1 | Unicode version |
Description: Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
Ref | Expression |
---|---|
simpll1 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | simpl1 969 | . 2 | |
2 | 1 | adantr 274 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 wa 103 w3a 947 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 |
This theorem depends on definitions: df-bi 116 df-3an 949 |
This theorem is referenced by: fidifsnen 6732 ordiso2 6888 ctssdc 6966 addlocpr 7312 xltadd1 9627 hashun 10519 fimaxq 10541 xrmaxltsup 10995 dvdslegcd 11580 lcmledvds 11678 divgcdcoprm0 11709 rpexp 11758 iscnp4 12314 cnconst2 12329 blssps 12523 blss 12524 metcnp 12608 addcncntoplem 12647 cdivcncfap 12683 |
Copyright terms: Public domain | W3C validator |