MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  ad7antr Structured version   Visualization version   GIF version

Theorem ad7antr 734
Description: Deduction adding 7 conjuncts to antecedent. (Contributed by Mario Carneiro, 4-Jan-2017.) (Proof shortened by Wolf Lammen, 5-Apr-2022.)
Hypothesis
Ref Expression
ad2ant.1 (𝜑𝜓)
Assertion
Ref Expression
ad7antr ((((((((𝜑𝜒) ∧ 𝜃) ∧ 𝜏) ∧ 𝜂) ∧ 𝜁) ∧ 𝜎) ∧ 𝜌) → 𝜓)

Proof of Theorem ad7antr
StepHypRef Expression
1 ad2ant.1 . . 3 (𝜑𝜓)
21adantr 479 . 2 ((𝜑𝜒) → 𝜓)
32ad6antr 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