Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > simpll3 | GIF version |
Description: Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
Ref | Expression |
---|---|
simpll3 | ⊢ ((((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) → 𝜒) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | simpl3 971 | . 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 ax-ia3 107 |
This theorem depends on definitions: df-bi 116 df-3an 949 |
This theorem is referenced by: frirrg 4242 fidceq 6731 fidifsnen 6732 en2eqpr 6769 iunfidisj 6802 ordiso2 6888 addlocpr 7312 aptiprlemu 7416 xltadd1 9627 xlesubadd 9634 icoshftf1o 9742 fztri3or 9787 elfzonelfzo 9975 exp3val 10263 hashun 10519 subcn2 11048 divalglemeuneg 11547 dvdslegcd 11580 lcmledvds 11678 rpdvds 11707 cncongr2 11712 iuncld 12211 iscnp4 12314 cnpnei 12315 cnconst2 12329 cnpdis 12338 txcn 12371 blssps 12523 blss 12524 metcnp3 12607 metcnp 12608 |
Copyright terms: Public domain | W3C validator |