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

Theorem ad7antr 737
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 484 . 2 ((𝜑𝜒) → 𝜓)
32ad6antr 735 1 ((((((((𝜑𝜒) ∧ 𝜃) ∧ 𝜏) ∧ 𝜂) ∧ 𝜁) ∧ 𝜎) ∧ 𝜌) → 𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 399
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 210  df-an 400
This theorem is referenced by:  ad8antr  739  ad8antlr  740  simp-7l  788  catpropd  16974  natpropd  17241  ucncn  22894  tgcgrxfr  26315  tgbtwnconn1lem3  26371  tgbtwnconn1  26372  midexlem  26489  lnopp2hpgb  26560  trgcopy  26601  elrspunidl  31017  qsidomlem2  31037  lbsdiflsp0  31110  fedgmul  31115  zarcmplem  31234  sigapildsys  31529  afsval  32050  matunitlindflem1  35046  dffltz  39602
  Copyright terms: Public domain W3C validator