![]() |
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 494 | . 2 ⊢ (((((𝜑 ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) ∧ 𝜂) → 𝜓) |
3 | 2 | adantr 276 | 1 ⊢ ((((((𝜑 ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) ∧ 𝜂) ∧ 𝜁) → 𝜓) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ wa 104 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 |
This theorem is referenced by: ad6antr 498 difinfinf 7103 ctssdclemn0 7112 cauappcvgprlemladdfu 7656 caucvgprlemloc 7677 caucvgprlemladdfu 7679 caucvgprlemlim 7683 caucvgprprlemml 7696 caucvgprprlemloc 7705 caucvgprprlemlim 7713 suplocexprlemmu 7720 suplocexprlemru 7721 suplocexprlemloc 7723 suplocsrlem 7810 axcaucvglemres 7901 nn0ltexp2 10692 resqrexlemglsq 11034 xrmaxifle 11257 xrmaxiflemlub 11259 divalglemeuneg 11931 bezoutlemnewy 12000 ctiunctlemfo 12443 mhmmnd 12986 txmetcnp 14158 mulcncf 14231 suplociccreex 14242 cnplimclemr 14278 limccnpcntop 14284 lgsval 14545 |
Copyright terms: Public domain | W3C validator |