![]() |
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 738 | 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 742 ad9antlr 743 simp-8l 791 legso 28621 miriso 28692 midexlem 28714 opphl 28776 trgcopy 28826 inaghl 28867 cyc3conja 33159 elrgspnlem4 33234 rloccring 33256 ssdifidlprm 33465 mxidlirred 33479 qsdrngi 33502 1arithidom 33544 1arithufdlem3 33553 lbsdiflsp0 33653 dimkerim 33654 fedgmul 33658 constrelextdg2 33751 qtophaus 33796 zarcmplem 33841 afsval 34664 dffltz 42620 hoidmvle 46555 smfmullem3 46748 |
Copyright terms: Public domain | W3C validator |