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 991 | . 2 ⊢ (((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃) → 𝜒) | |
2 | 1 | adantr 274 | 1 ⊢ ((((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) → 𝜒) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ wa 103 ∧ w3a 967 |
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 969 |
This theorem is referenced by: frirrg 4322 fidceq 6826 fidifsnen 6827 en2eqpr 6864 iunfidisj 6902 ordiso2 6991 addlocpr 7468 aptiprlemu 7572 xltadd1 9803 xlesubadd 9810 icoshftf1o 9918 fztri3or 9964 elfzonelfzo 10155 exp3val 10447 nn0ltexp2 10612 hashun 10707 subcn2 11238 divalglemeuneg 11845 dvdslegcd 11882 lcmledvds 11981 rpdvds 12010 cncongr2 12015 qexpz 12261 iuncld 12662 iscnp4 12765 cnpnei 12766 cnconst2 12780 cnpdis 12789 txcn 12822 blssps 12974 blss 12975 metcnp3 13058 metcnp 13059 |
Copyright terms: Public domain | W3C validator |