![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > ad7antr | Structured version Visualization version GIF version |
Description: Deduction adding 7 conjuncts to antecedent. (Contributed by Mario Carneiro, 4-Jan-2017.) (Proof shortened by Wolf Lammen, 5-Apr-2022.) |
Ref | Expression |
---|---|
ad2ant.1 | ⊢ (𝜑 → 𝜓) |
Ref | Expression |
---|---|
ad7antr | ⊢ ((((((((𝜑 ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) ∧ 𝜂) ∧ 𝜁) ∧ 𝜎) ∧ 𝜌) → 𝜓) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ad2ant.1 | . . 3 ⊢ (𝜑 → 𝜓) | |
2 | 1 | adantr 481 | . 2 ⊢ ((𝜑 ∧ 𝜒) → 𝜓) |
3 | 2 | ad6antr 734 | 1 ⊢ ((((((((𝜑 ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) ∧ 𝜂) ∧ 𝜁) ∧ 𝜎) ∧ 𝜌) → 𝜓) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 396 |
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 397 |
This theorem is referenced by: ad8antr 738 ad8antlr 739 simp-7l 787 catpropd 17588 natpropd 17864 ucncn 23635 tgcgrxfr 27407 tgbtwnconn1lem3 27463 tgbtwnconn1 27464 midexlem 27581 lnopp2hpgb 27652 trgcopy 27693 mgcf1o 31807 elrspunidl 32143 rhmimaidl 32146 qsidomlem2 32166 lbsdiflsp0 32261 fedgmul 32266 zarcmplem 32402 sigapildsys 32701 afsval 33224 matunitlindflem1 36064 dffltz 40949 |
Copyright terms: Public domain | W3C validator |