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

Theorem ad5antr 765
Description: Deduction adding 5 conjuncts to antecedent. (Contributed by Mario Carneiro, 4-Jan-2017.)
Hypothesis
Ref Expression
ad2ant.1 (𝜑𝜓)
Assertion
Ref Expression
ad5antr ((((((𝜑𝜒) ∧ 𝜃) ∧ 𝜏) ∧ 𝜂) ∧ 𝜁) → 𝜓)

Proof of Theorem ad5antr
StepHypRef Expression
1 ad2ant.1 . . 3 (𝜑𝜓)
21ad4antr 763 . 2 (((((𝜑𝜒) ∧ 𝜃) ∧ 𝜏) ∧ 𝜂) → 𝜓)
32adantr 479 1 ((((((𝜑𝜒) ∧ 𝜃) ∧ 𝜏) ∧ 𝜂) ∧ 𝜁) → 𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 382
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 195  df-an 384
This theorem is referenced by:  ad6antr  767  catass  16118  catpropd  16140  cidpropd  16141  monpropd  16168  funcpropd  16331  fucpropd  16408  drsdirfi  16709  mhmmnd  17308  neitr  20741  xkoccn  21179  trust  21790  restutopopn  21799  ucncn  21846  trcfilu  21855  ulmcau  23897  lgamucov  24508  tgcgrxfr  25158  tgbtwnconn1  25215  legov  25225  legso  25239  midexlem  25332  perpneq  25354  footex  25358  colperpexlem3  25369  colperpex  25370  opphllem  25372  opphllem3  25386  outpasch  25392  hlpasch  25393  lmieu  25421  trgcopy  25441  trgcopyeu  25443  dfcgra2  25466  acopyeu  25470  cgrg3col4  25479  f1otrg  25496  pthdepisspth  25897  omndmul2  28836  fimaproj  29021  qtophaus  29024  locfinreflem  29028  matunitlindflem1  32358  heicant  32397  mblfinlem3  32401  mblfinlem4  32402  itg2gt0cn  32418  sstotbnd2  32526  pell1234qrdich  36226  supxrgelem  38277  icccncfext  38556  etransclem35  38945  smflimlem2  39441
  Copyright terms: Public domain W3C validator