Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > simpll1 | GIF version |
Description: Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
Ref | Expression |
---|---|
simpll1 | ⊢ ((((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) → 𝜑) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | simpl1 996 | . 2 ⊢ (((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃) → 𝜑) | |
2 | 1 | adantr 274 | 1 ⊢ ((((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) → 𝜑) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ wa 103 ∧ w3a 974 |
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 976 |
This theorem is referenced by: fidifsnen 6852 ordiso2 7016 ctssdc 7094 addlocpr 7502 xltadd1 9837 nn0ltexp2 10648 hashun 10744 fimaxq 10766 xrmaxltsup 11225 dvdslegcd 11923 lcmledvds 12028 divgcdcoprm0 12059 rpexp 12111 qexpz 12308 dfgrp3mlem 12801 iscnp4 13097 cnconst2 13112 blssps 13306 blss 13307 metcnp 13391 addcncntoplem 13430 cdivcncfap 13466 lgsfvalg 13785 lgsmod 13806 lgsdir 13815 lgsne0 13818 |
Copyright terms: Public domain | W3C validator |