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

Theorem ad5antr 773
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 480 . 2 ((𝜑𝜒) → 𝜓)
32ad4antr 769 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  777  ad6antrOLD  778  ad6antlr  779  catass  16394  catpropd  16416  cidpropd  16417  monpropd  16444  funcpropd  16607  fucpropd  16684  drsdirfi  16985  mhmmnd  17584  neitr  21032  xkoccn  21470  trust  22080  restutopopn  22089  ucncn  22136  trcfilu  22145  ulmcau  24194  lgamucov  24809  tgcgrxfr  25458  tgbtwnconn1  25515  legov  25525  legso  25539  midexlem  25632  perpneq  25654  footex  25658  colperpexlem3  25669  colperpex  25670  opphllem  25672  opphllem3  25686  outpasch  25692  hlpasch  25693  lmieu  25721  trgcopy  25741  trgcopyeu  25743  dfcgra2  25766  acopyeu  25770  cgrg3col4  25779  f1otrg  25796  omndmul2  29840  fimaproj  30028  qtophaus  30031  locfinreflem  30035  hgt750lemb  30862  matunitlindflem1  33535  heicant  33574  mblfinlem3  33578  mblfinlem4  33579  itg2gt0cn  33595  sstotbnd2  33703  pell1234qrdich  37742  supxrgelem  39866  icccncfext  40418  etransclem35  40804  smflimlem2  41301
  Copyright terms: Public domain W3C validator