![]() |
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 482 | . 2 ⊢ ((𝜒 ∧ 𝜑) → 𝜓) |
3 | 2 | ad4antr 730 | 1 ⊢ ((((((𝜒 ∧ 𝜑) ∧ 𝜃) ∧ 𝜏) ∧ 𝜂) ∧ 𝜁) → 𝜓) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 396 |
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 206 df-an 397 |
This theorem is referenced by: simp-5r 784 fimaproj 8123 restmetu 24086 foresf1o 31780 2ndresdju 31912 nn0xmulclb 32022 isdrng4 32436 elrspunidl 32591 elrspunsn 32592 rhmpreimaprmidl 32615 fedgmul 32775 locfinreflem 32889 pstmxmet 32946 satfdmlem 34428 mblfinlem3 36613 itg2gt0cn 36629 dffltz 41458 pell1234qrmulcl 41675 suplesup 44128 limclner 44446 bgoldbtbnd 46556 isomushgr 46573 |
Copyright terms: Public domain | W3C validator |