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 989 | . 2 | |
2 | 1 | adantr 274 | 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 |
This theorem depends on definitions: df-bi 116 df-3an 969 |
This theorem is referenced by: fidifsnen 6827 ordiso2 6991 ctssdc 7069 addlocpr 7468 xltadd1 9803 nn0ltexp2 10612 hashun 10707 fimaxq 10729 xrmaxltsup 11185 dvdslegcd 11882 lcmledvds 11981 divgcdcoprm0 12012 rpexp 12064 qexpz 12261 iscnp4 12765 cnconst2 12780 blssps 12974 blss 12975 metcnp 13059 addcncntoplem 13098 cdivcncfap 13134 |
Copyright terms: Public domain | W3C validator |