| 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 28607 miriso 28678 midexlem 28700 opphl 28762 trgcopy 28812 inaghl 28853 cyc3conja 33177 elrgspnlem4 33249 rloccring 33274 ssdifidlprm 33486 mxidlirred 33500 qsdrngi 33523 1arithidom 33565 1arithufdlem3 33574 lbsdiflsp0 33677 dimkerim 33678 fedgmul 33682 constrelextdg2 33788 qtophaus 33835 zarcmplem 33880 afsval 34686 dffltz 42644 hoidmvle 46615 smfmullem3 46808 |
| Copyright terms: Public domain | W3C validator |