![]() |
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 480 | . 2 ⊢ ((𝜑 ∧ 𝜒) → 𝜓) |
3 | 2 | ad6antr 736 | 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: ad8antr 740 ad8antlr 741 simp-7l 789 catpropd 17753 natpropd 18032 ucncn 24309 tgcgrxfr 28540 tgbtwnconn1lem3 28596 tgbtwnconn1 28597 midexlem 28714 lnopp2hpgb 28785 trgcopy 28826 mgcf1o 32977 chnub 32985 elrgspnlem4 33234 elrspunidl 33435 rhmimaidl 33439 qsidomlem2 33460 ssdifidlprm 33465 mxidlirredi 33478 1arithufdlem3 33553 lbsdiflsp0 33653 fedgmul 33658 constrconj 33749 constrelextdg2 33751 zarcmplem 33841 sigapildsys 34142 afsval 34664 matunitlindflem1 37602 aks6d1c2lem4 42108 dffltz 42620 |
Copyright terms: Public domain | W3C validator |