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

Theorem ad5antr 732
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 481 . 2 ((𝜑𝜒) → 𝜓)
32ad4antr 730 1 ((((((𝜑𝜒) ∧ 𝜃) ∧ 𝜏) ∧ 𝜂) ∧ 𝜁) → 𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396
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 206  df-an 397
This theorem is referenced by:  ad6antr  734  ad6antlr  735  simp-5l  783  fimaproj  8063  catass  17558  catpropd  17581  cidpropd  17582  monpropd  17612  funcpropd  17779  fucpropd  17858  drsdirfi  18186  mhmmnd  18860  neitr  22515  xkoccn  22954  trust  23565  restutopopn  23574  ucncn  23621  trcfilu  23630  ulmcau  25738  lgamucov  26371  tgcgrxfr  27346  tgbtwnconn1  27403  legov  27413  legso  27427  midexlem  27520  perpneq  27542  footexALT  27546  footex  27549  colperpexlem3  27560  colperpex  27561  opphllem  27563  opphllem3  27577  outpasch  27583  hlpasch  27584  lmieu  27612  trgcopy  27632  trgcopyeu  27634  dfcgra2  27658  acopyeu  27662  cgrg3col4  27681  f1otrg  27699  fnpreimac  31473  nn0xmulclb  31559  s3f1  31686  omndmul2  31803  cyc3conja  31889  nsgqusf1olem3  32076  rhmimaidl  32085  mxidlprm  32116  ssmxidllem  32117  fedgmul  32203  extdg1id  32229  qtophaus  32286  locfinreflem  32290  zarclssn  32323  hgt750lemb  33138  matunitlindflem1  36041  heicant  36080  mblfinlem3  36084  mblfinlem4  36085  itg2gt0cn  36100  sstotbnd2  36200  aks4d1p8  40511  aks6d1c2p2  40516  fsuppind  40703  pell1234qrdich  41122  omabs2  41603  supxrgelem  43507  icccncfext  44060  etransclem35  44442  smflimlem2  44945
  Copyright terms: Public domain W3C validator