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

Theorem ad7antr 738
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 480 . 2 ((𝜑𝜒) → 𝜓)
32ad6antr 736 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:  ad8antr  740  ad8antlr  741  simp-7l  789  catpropd  17753  natpropd  18032  ucncn  24309  tgcgrxfr  28540  tgbtwnconn1lem3  28596  tgbtwnconn1  28597  midexlem  28714  lnopp2hpgb  28785  trgcopy  28826  mgcf1o  32977  chnub  32985  elrgspnlem4  33234  elrspunidl  33435  rhmimaidl  33439  qsidomlem2  33460  ssdifidlprm  33465  mxidlirredi  33478  1arithufdlem3  33553  lbsdiflsp0  33653  fedgmul  33658  constrconj  33749  constrelextdg2  33751  zarcmplem  33841  sigapildsys  34142  afsval  34664  matunitlindflem1  37602  aks6d1c2lem4  42108  dffltz  42620
  Copyright terms: Public domain W3C validator