![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > ad8antr | Structured version Visualization version GIF version |
Description: Deduction adding 8 conjuncts to antecedent. (Contributed by Mario Carneiro, 4-Jan-2017.) (Proof shortened by Wolf Lammen, 5-Apr-2022.) |
Ref | Expression |
---|---|
ad2ant.1 | ⊢ (𝜑 → 𝜓) |
Ref | Expression |
---|---|
ad8antr | ⊢ (((((((((𝜑 ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) ∧ 𝜂) ∧ 𝜁) ∧ 𝜎) ∧ 𝜌) ∧ 𝜇) → 𝜓) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ad2ant.1 | . . 3 ⊢ (𝜑 → 𝜓) | |
2 | 1 | adantr 480 | . 2 ⊢ ((𝜑 ∧ 𝜒) → 𝜓) |
3 | 2 | ad7antr 737 | 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 207 df-an 396 |
This theorem is referenced by: ad9antr 741 ad9antlr 742 simp-8l 790 legso 28625 miriso 28696 midexlem 28718 opphl 28780 trgcopy 28830 inaghl 28871 cyc3conja 33150 rloccring 33242 ssdifidlprm 33451 mxidlirred 33465 qsdrngi 33488 1arithidom 33530 1arithufdlem3 33539 lbsdiflsp0 33639 dimkerim 33640 fedgmul 33644 constrelextdg2 33737 qtophaus 33782 zarcmplem 33827 afsval 34648 dffltz 42589 hoidmvle 46521 smfmullem3 46714 |
Copyright terms: Public domain | W3C validator |