Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > simpll3 | Unicode version |
Description: Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
Ref | Expression |
---|---|
simpll3 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | simpl3 997 | . 2 | |
2 | 1 | adantr 274 | 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: frirrg 4335 fidceq 6847 fidifsnen 6848 en2eqpr 6885 iunfidisj 6923 ordiso2 7012 addlocpr 7498 aptiprlemu 7602 xltadd1 9833 xlesubadd 9840 icoshftf1o 9948 fztri3or 9995 elfzonelfzo 10186 exp3val 10478 nn0ltexp2 10644 hashun 10740 subcn2 11274 divalglemeuneg 11882 dvdslegcd 11919 lcmledvds 12024 rpdvds 12053 cncongr2 12058 qexpz 12304 iuncld 12909 iscnp4 13012 cnpnei 13013 cnconst2 13027 cnpdis 13036 txcn 13069 blssps 13221 blss 13222 metcnp3 13305 metcnp 13306 lgsfcl2 13701 lgsdir 13730 lgsne0 13733 |
Copyright terms: Public domain | W3C validator |