![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > ad5antr | GIF version |
Description: Deduction adding 5 conjuncts to antecedent. (Contributed by Mario Carneiro, 4-Jan-2017.) |
Ref | Expression |
---|---|
ad2ant.1 | ⊢ (𝜑 → 𝜓) |
Ref | Expression |
---|---|
ad5antr | ⊢ ((((((𝜑 ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) ∧ 𝜂) ∧ 𝜁) → 𝜓) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ad2ant.1 | . . 3 ⊢ (𝜑 → 𝜓) | |
2 | 1 | ad4antr 486 | . 2 ⊢ (((((𝜑 ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) ∧ 𝜂) → 𝜓) |
3 | 2 | adantr 274 | 1 ⊢ ((((((𝜑 ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) ∧ 𝜂) ∧ 𝜁) → 𝜓) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ wa 103 |
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 is referenced by: ad6antr 490 difinfinf 6994 ctssdclemn0 7003 cauappcvgprlemladdfu 7486 caucvgprlemloc 7507 caucvgprlemladdfu 7509 caucvgprlemlim 7513 caucvgprprlemml 7526 caucvgprprlemloc 7535 caucvgprprlemlim 7543 suplocexprlemmu 7550 suplocexprlemru 7551 suplocexprlemloc 7553 suplocsrlem 7640 axcaucvglemres 7731 resqrexlemglsq 10826 xrmaxifle 11047 xrmaxiflemlub 11049 divalglemeuneg 11656 bezoutlemnewy 11720 ctiunctlemfo 11988 txmetcnp 12726 mulcncf 12799 suplociccreex 12810 cnplimclemr 12846 limccnpcntop 12852 |
Copyright terms: Public domain | W3C validator |