|   | Metamath Proof Explorer | < Previous  
      Next > Nearby theorems | |
| Mirrors > Home > MPE Home > Th. List > ad6antr | Structured version Visualization version GIF version | ||
| Description: Deduction adding 6 conjuncts to antecedent. (Contributed by Mario Carneiro, 4-Jan-2017.) (Proof shortened by Wolf Lammen, 5-Apr-2022.) | 
| Ref | Expression | 
|---|---|
| ad2ant.1 | ⊢ (𝜑 → 𝜓) | 
| Ref | Expression | 
|---|---|
| ad6antr | ⊢ (((((((𝜑 ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) ∧ 𝜂) ∧ 𝜁) ∧ 𝜎) → 𝜓) | 
| Step | Hyp | Ref | Expression | 
|---|---|---|---|
| 1 | ad2ant.1 | . . 3 ⊢ (𝜑 → 𝜓) | |
| 2 | 1 | adantr 480 | . 2 ⊢ ((𝜑 ∧ 𝜒) → 𝜓) | 
| 3 | 2 | ad5antr 734 | 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: ad7antr 738 ad7antlr 739 simp-6l 786 catass 17730 funcpropd 17948 natpropd 18025 ghmqusnsg 19301 ghmquskerlem3 19305 rhmqusnsg 21296 restutop 24247 utopreg 24262 restmetu 24584 lgamucov 27082 istrkgcb 28465 tgifscgr 28517 tgbtwnconn1lem3 28583 legtrd 28598 miriso 28679 footexALT 28727 footex 28730 opphllem3 28758 opphl 28763 trgcopy 28813 cgratr 28832 dfcgra2 28839 inaghl 28854 cgrg3col4 28862 f1otrge 28881 clwlkclwwlklem2 30020 gsumwun 33069 cyc3genpm 33173 elrgspnlem4 33250 erler 33270 rlocaddval 33273 rlocmulval 33274 rloccring 33275 rhmquskerlem 33454 elrspunidl 33457 rhmimaidl 33461 ssdifidllem 33485 ssdifidlprm 33487 mxidlirredi 33500 mxidlirred 33501 ssmxidllem 33502 qsdrngi 33524 1arithidom 33566 1arithufdlem3 33575 r1plmhm 33631 r1pquslmic 33632 lbsdiflsp0 33678 dimkerim 33679 fedgmul 33683 fldextrspunlsplem 33724 fldext2chn 33770 constrextdg2lem 33790 txomap 33834 matunitlindflem1 37624 heicant 37663 mblfinlem3 37667 primrootscoprmpow 42101 aks6d1c2lem4 42129 aks6d1c5 42141 limclner 45671 hoidmvle 46620 | 
| Copyright terms: Public domain | W3C validator |