Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > simpll2 | GIF version |
Description: Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
Ref | Expression |
---|---|
simpll2 | ⊢ ((((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) → 𝜓) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | simpl2 985 | . 2 ⊢ (((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃) → 𝜓) | |
2 | 1 | adantr 274 | 1 ⊢ ((((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) → 𝜓) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ wa 103 ∧ w3a 962 |
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 964 |
This theorem is referenced by: fidceq 6756 fidifsnen 6757 en2eqpr 6794 iunfidisj 6827 ctssdc 6991 cauappcvgprlemlol 7448 caucvgprlemlol 7471 caucvgprprlemlol 7499 elfzonelfzo 10000 qbtwnre 10027 hashun 10544 xrmaxltsup 11020 subcn2 11073 divalglemex 11608 divalglemeuneg 11609 dvdslegcd 11642 lcmledvds 11740 iscnp4 12376 cnrest2 12394 blssps 12585 blss 12586 bdbl 12661 metcnp3 12669 addcncntoplem 12709 cdivcncfap 12745 |
Copyright terms: Public domain | W3C validator |