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 485 | . 2 ⊢ ((𝜒 ∧ 𝜑) → 𝜓) |
3 | 2 | ad4antr 732 | 1 ⊢ ((((((𝜒 ∧ 𝜑) ∧ 𝜃) ∧ 𝜏) ∧ 𝜂) ∧ 𝜁) → 𝜓) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 399 |
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 210 df-an 400 |
This theorem is referenced by: simp-5r 786 fimaproj 7902 restmetu 23468 foresf1o 30569 2ndresdju 30705 nn0xmulclb 30814 elrspunidl 31320 rhmpreimaprmidl 31341 fedgmul 31426 locfinreflem 31504 pstmxmet 31561 satfdmlem 33043 mblfinlem3 35553 itg2gt0cn 35569 dffltz 40174 pell1234qrmulcl 40380 suplesup 42551 limclner 42867 bgoldbtbnd 44934 isomushgr 44951 |
Copyright terms: Public domain | W3C validator |