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

Theorem ad5antr 775
Description: Deduction adding 5 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
ad5antr ((((((𝜑𝜒) ∧ 𝜃) ∧ 𝜏) ∧ 𝜂) ∧ 𝜁) → 𝜓)

Proof of Theorem ad5antr
StepHypRef Expression
1 ad2ant.1 . . 3 (𝜑𝜓)
21adantr 472 . 2 ((𝜑𝜒) → 𝜓)
32ad4antr 771 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:  ad6antr  779  ad6antrOLD  780  ad6antlr  781  simp-5l  829  simp-6r  835  catass  16568  catpropd  16590  cidpropd  16591  monpropd  16618  funcpropd  16781  fucpropd  16858  drsdirfi  17159  mhmmnd  17758  neitr  21206  xkoccn  21644  trust  22254  restutopopn  22263  ucncn  22310  trcfilu  22319  ulmcau  24368  lgamucov  24984  tgcgrxfr  25633  tgbtwnconn1  25690  legov  25700  legso  25714  midexlem  25807  perpneq  25829  footex  25833  colperpexlem3  25844  colperpex  25845  opphllem  25847  opphllem3  25861  outpasch  25867  hlpasch  25868  lmieu  25896  trgcopy  25916  trgcopyeu  25918  dfcgra2  25941  acopyeu  25945  cgrg3col4  25954  f1otrg  25971  omndmul2  30042  fimaproj  30230  qtophaus  30233  locfinreflem  30237  hgt750lemb  31064  matunitlindflem1  33736  heicant  33775  mblfinlem3  33779  mblfinlem4  33780  itg2gt0cn  33796  sstotbnd2  33904  pell1234qrdich  37945  supxrgelem  40069  icccncfext  40621  etransclem35  41007  smflimlem2  41504
  Copyright terms: Public domain W3C validator