| 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 17752 natpropd 18024 ucncn 24294 tgcgrxfr 28526 tgbtwnconn1lem3 28582 tgbtwnconn1 28583 midexlem 28700 lnopp2hpgb 28771 trgcopy 28812 mgcf1o 32993 chnub 33002 elrgspnlem4 33249 elrspunidl 33456 rhmimaidl 33460 qsidomlem2 33481 ssdifidlprm 33486 mxidlirredi 33499 1arithufdlem3 33574 lbsdiflsp0 33677 fedgmul 33682 constrconj 33786 constrelextdg2 33788 zarcmplem 33880 sigapildsys 34163 afsval 34686 matunitlindflem1 37623 aks6d1c2lem4 42128 dffltz 42644 |
| Copyright terms: Public domain | W3C validator |