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

Theorem ad6antr 777
Description: Deduction adding 6 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
ad6antr (((((((𝜑𝜒) ∧ 𝜃) ∧ 𝜏) ∧ 𝜂) ∧ 𝜁) ∧ 𝜎) → 𝜓)

Proof of Theorem ad6antr
StepHypRef Expression
1 ad2ant.1 . . 3 (𝜑𝜓)
21adantr 480 . 2 ((𝜑𝜒) → 𝜓)
32ad5antr 773 1 (((((((𝜑𝜒) ∧ 𝜃) ∧ 𝜏) ∧ 𝜂) ∧ 𝜁) ∧ 𝜎) → 𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 383
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 197  df-an 385
This theorem is referenced by:  ad7antr  781  ad7antrOLD  782  ad7antlr  783  catass  16394  funcpropd  16607  natpropd  16683  restutop  22088  utopreg  22103  restmetu  22422  lgamucov  24809  istrkgcb  25400  tgifscgr  25448  tgbtwnconn1lem3  25514  legtrd  25529  miriso  25610  footex  25658  opphllem3  25686  opphl  25691  trgcopy  25741  cgratr  25760  dfcgra2  25766  inaghl  25776  cgrg3col4  25779  f1otrge  25797  clwlkclwwlklem2  26966  matunitlindflem1  33535  heicant  33574  mblfinlem3  33578  limclner  40201  hoidmvle  41135
  Copyright terms: Public domain W3C validator