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 970 | . 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: fidceq 6731 fidifsnen 6732 en2eqpr 6769 iunfidisj 6802 ctssdc 6966 cauappcvgprlemlol 7423 caucvgprlemlol 7446 caucvgprprlemlol 7474 elfzonelfzo 9975 qbtwnre 10002 hashun 10519 xrmaxltsup 10995 subcn2 11048 divalglemex 11546 divalglemeuneg 11547 dvdslegcd 11580 lcmledvds 11678 iscnp4 12314 cnrest2 12332 blssps 12523 blss 12524 bdbl 12599 metcnp3 12607 addcncntoplem 12647 cdivcncfap 12683 |
Copyright terms: Public domain | W3C validator |