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

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

Proof of Theorem ad4antlr
StepHypRef Expression
1 ad2ant.1 . . 3 (𝜑𝜓)
21ad3antlr 763 . 2 ((((𝜒𝜑) ∧ 𝜃) ∧ 𝜏) → 𝜓)
32adantr 480 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 196  df-an 385
This theorem is referenced by:  ad5antlr  767  initoeu2  16489  cpmatacl  20340  cpmatmcllem  20342  cpmatmcl  20343  chfacfisf  20478  chfacfisfcpmat  20479  restcld  20786  pthaus  21251  txhaus  21260  xkohaus  21266  alexsubALTlem4  21664  ustuqtop3  21857  ulmcau  23953  usgra2wlkspth  26149  clwlkisclwwlklem1  26315  usg2spot2nb  26592  locfinreflem  29235  cmpcref  29245  pstmxmet  29268  sigapildsys  29552  ldgenpisyslem1  29553  nn0prpwlem  31487  matunitlindflem1  32575  matunitlindflem2  32576  poimirlem29  32608  heicant  32614  mblfinlem3  32618  mblfinlem4  32619  itg2addnclem2  32632  itg2gt0cn  32635  ftc1cnnc  32654  sstotbnd2  32743  pell1234qrdich  36443  jm2.26lem3  36586  cvgdvgrat  37534  icccncfext  38773  fourierdlem34  39034  fourierdlem87  39086  etransclem35  39162  smfaddlem1  39649  sfprmdvdsmersenne  40058  bgoldbwt  40199  bgoldbtbnd  40225  clwlkclwwlklem2  41209  ply1mulgsumlem2  41969  nn0sumshdiglemA  42211
  Copyright terms: Public domain W3C validator