![]() |
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 479 | . 2 ⊢ ((𝜑 ∧ 𝜒) → 𝜓) |
3 | 2 | ad6antr 732 | 1 ⊢ ((((((((𝜑 ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) ∧ 𝜂) ∧ 𝜁) ∧ 𝜎) ∧ 𝜌) → 𝜓) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 394 |
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 395 |
This theorem is referenced by: ad8antr 736 ad8antlr 737 simp-7l 785 catpropd 17657 natpropd 17933 ucncn 24010 tgcgrxfr 28036 tgbtwnconn1lem3 28092 tgbtwnconn1 28093 midexlem 28210 lnopp2hpgb 28281 trgcopy 28322 mgcf1o 32440 elrspunidl 32820 rhmimaidl 32824 qsidomlem2 32846 mxidlirredi 32861 lbsdiflsp0 32999 fedgmul 33004 zarcmplem 33159 sigapildsys 33458 afsval 33981 matunitlindflem1 36787 dffltz 41678 |
Copyright terms: Public domain | W3C validator |