![]() |
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 7099 ctssdclemn0 7108 cauappcvgprlemladdfu 7652 caucvgprlemloc 7673 caucvgprlemladdfu 7675 caucvgprlemlim 7679 caucvgprprlemml 7692 caucvgprprlemloc 7701 caucvgprprlemlim 7709 suplocexprlemmu 7716 suplocexprlemru 7717 suplocexprlemloc 7719 suplocsrlem 7806 axcaucvglemres 7897 nn0ltexp2 10685 resqrexlemglsq 11026 xrmaxifle 11249 xrmaxiflemlub 11251 divalglemeuneg 11922 bezoutlemnewy 11991 ctiunctlemfo 12434 mhmmnd 12934 txmetcnp 13911 mulcncf 13984 suplociccreex 13995 cnplimclemr 14031 limccnpcntop 14037 lgsval 14298 |
Copyright terms: Public domain | W3C validator |