Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > ad5antlr | Structured version Visualization version GIF version |
Description: Deduction adding 5 conjuncts to antecedent. (Contributed by Mario Carneiro, 5-Jan-2017.) (Proof shortened by Wolf Lammen, 5-Apr-2022.) |
Ref | Expression |
---|---|
ad2ant.1 | ⊢ (𝜑 → 𝜓) |
Ref | Expression |
---|---|
ad5antlr | ⊢ ((((((𝜒 ∧ 𝜑) ∧ 𝜃) ∧ 𝜏) ∧ 𝜂) ∧ 𝜁) → 𝜓) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ad2ant.1 | . . 3 ⊢ (𝜑 → 𝜓) | |
2 | 1 | adantl 484 | . 2 ⊢ ((𝜒 ∧ 𝜑) → 𝜓) |
3 | 2 | ad4antr 730 | 1 ⊢ ((((((𝜒 ∧ 𝜑) ∧ 𝜃) ∧ 𝜏) ∧ 𝜂) ∧ 𝜁) → 𝜓) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 398 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 |
This theorem depends on definitions: df-bi 209 df-an 399 |
This theorem is referenced by: simp-5r 784 fimaproj 7815 restmetu 23163 foresf1o 30250 nn0xmulclb 30482 fedgmul 31037 locfinreflem 31114 pstmxmet 31147 satfdmlem 32622 mblfinlem3 34965 itg2gt0cn 34981 dffltz 39363 pell1234qrmulcl 39544 suplesup 41697 limclner 42022 bgoldbtbnd 44059 isomushgr 44076 |
Copyright terms: Public domain | W3C validator |