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

Theorem ad7antr 736
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 481 . 2 ((𝜑𝜒) → 𝜓)
32ad6antr 734 1 ((((((((𝜑𝜒) ∧ 𝜃) ∧ 𝜏) ∧ 𝜂) ∧ 𝜁) ∧ 𝜎) ∧ 𝜌) → 𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396
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 397
This theorem is referenced by:  ad8antr  738  ad8antlr  739  simp-7l  787  catpropd  17588  natpropd  17864  ucncn  23635  tgcgrxfr  27407  tgbtwnconn1lem3  27463  tgbtwnconn1  27464  midexlem  27581  lnopp2hpgb  27652  trgcopy  27693  mgcf1o  31807  elrspunidl  32143  rhmimaidl  32146  qsidomlem2  32166  lbsdiflsp0  32261  fedgmul  32266  zarcmplem  32402  sigapildsys  32701  afsval  33224  matunitlindflem1  36064  dffltz  40949
  Copyright terms: Public domain W3C validator