![]() |
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 481 | . 2 ⊢ ((𝜒 ∧ 𝜑) → 𝜓) |
3 | 2 | ad4antr 731 | 1 ⊢ ((((((𝜒 ∧ 𝜑) ∧ 𝜃) ∧ 𝜏) ∧ 𝜂) ∧ 𝜁) → 𝜓) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 395 |
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 396 |
This theorem is referenced by: simp-5r 785 fimaproj 8134 restmetu 24466 foresf1o 32286 2ndresdju 32418 nn0xmulclb 32525 isdrng4 32932 elrspunidl 33079 elrspunsn 33080 rhmpreimaprmidl 33103 fedgmul 33261 locfinreflem 33377 pstmxmet 33434 satfdmlem 34914 mblfinlem3 37067 itg2gt0cn 37083 dffltz 41980 pell1234qrmulcl 42197 suplesup 44644 limclner 44962 bgoldbtbnd 47072 gricushgr 47106 |
Copyright terms: Public domain | W3C validator |