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 485 | . 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 489 difinfinf 6954 ctssdclemn0 6963 cauappcvgprlemladdfu 7430 caucvgprlemloc 7451 caucvgprlemladdfu 7453 caucvgprlemlim 7457 caucvgprprlemml 7470 caucvgprprlemloc 7479 caucvgprprlemlim 7487 suplocexprlemmu 7494 suplocexprlemru 7495 suplocexprlemloc 7497 suplocsrlem 7584 axcaucvglemres 7675 resqrexlemglsq 10762 xrmaxifle 10983 xrmaxiflemlub 10985 divalglemeuneg 11547 bezoutlemnewy 11611 ctiunctlemfo 11879 txmetcnp 12614 mulcncf 12687 suplociccreex 12698 cnplimclemr 12734 limccnpcntop 12740 |
Copyright terms: Public domain | W3C validator |