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

Theorem ad4antlr 732
Description: Deduction adding 4 conjuncts to antecedent. (Contributed by Mario Carneiro, 5-Jan-2017.) (Proof shortened by Wolf Lammen, 5-Apr-2022.)
Hypothesis
Ref Expression
ad2ant.1 (𝜑𝜓)
Assertion
Ref Expression
ad4antlr (((((𝜒𝜑) ∧ 𝜃) ∧ 𝜏) ∧ 𝜂) → 𝜓)

Proof of Theorem ad4antlr
StepHypRef Expression
1 ad2ant.1 . . 3 (𝜑𝜓)
21adantl 485 . 2 ((𝜒𝜑) → 𝜓)
32ad3antrrr 729 1 (((((𝜒𝜑) ∧ 𝜃) ∧ 𝜏) ∧ 𝜂) → 𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 399
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 210  df-an 400
This theorem is referenced by:  simp-4r  783  initoeu2  17267  cpmatacl  21319  cpmatmcllem  21321  cpmatmcl  21322  chfacfisf  21457  chfacfisfcpmat  21458  restcld  21775  pthaus  22241  txhaus  22250  xkohaus  22256  alexsubALTlem4  22653  ustuqtop3  22847  ulmcau  24988  2sqreulem1  26028  2sqreunnlem1  26031  clwlkclwwlklem2  27783  qsidomlem1  31007  dimkerim  31080  fedgmul  31084  locfinreflem  31162  cmpcref  31172  pstmxmet  31214  sigapildsys  31495  ldgenpisyslem1  31496  signstfvneq0  31916  nn0prpwlem  33744  matunitlindflem1  35011  matunitlindflem2  35012  poimirlem29  35044  heicant  35050  mblfinlem3  35054  mblfinlem4  35055  itg2addnclem2  35067  itg2gt0cn  35070  ftc1cnnc  35087  sstotbnd2  35170  pell1234qrdich  39732  jm2.26lem3  39872  cvgdvgrat  40951  limsupgtlem  42358  limsupub2  42393  xlimmnfv  42415  icccncfext  42468  fourierdlem34  42722  fourierdlem87  42774  etransclem35  42850  smfaddlem1  43335  sfprmdvdsmersenne  44060  sbgoldbwt  44234  bgoldbtbnd  44266  ply1mulgsumlem2  44734  nn0sumshdiglemA  44972
  Copyright terms: Public domain W3C validator