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  16438  cpmatacl  20288  cpmatmcllem  20290  cpmatmcl  20291  chfacfisf  20426  chfacfisfcpmat  20427  restcld  20734  pthaus  21199  txhaus  21208  xkohaus  21214  alexsubALTlem4  21612  ustuqtop3  21805  ulmcau  23898  usgra2wlkspth  25943  clwlkisclwwlklem1  26109  usg2spot2nb  26386  locfinreflem  29029  cmpcref  29039  pstmxmet  29062  sigapildsys  29346  ldgenpisyslem1  29347  nn0prpwlem  31281  matunitlindflem1  32369  matunitlindflem2  32370  poimirlem29  32402  heicant  32408  mblfinlem3  32412  mblfinlem4  32413  itg2addnclem2  32426  itg2gt0cn  32429  ftc1cnnc  32448  sstotbnd2  32537  pell1234qrdich  36237  jm2.26lem3  36380  cvgdvgrat  37328  icccncfext  38567  fourierdlem34  38828  fourierdlem87  38880  etransclem35  38956  smfaddlem1  39443  sfprmdvdsmersenne  39853  bgoldbwt  39994  bgoldbtbnd  40020  clwlkclwwlklem2  41201  ply1mulgsumlem2  41961  nn0sumshdiglemA  42203
  Copyright terms: Public domain W3C validator