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 481 . 2 ((𝜒𝜑) → 𝜓)
32ad3antrrr 729 1 (((((𝜒𝜑) ∧ 𝜃) ∧ 𝜏) ∧ 𝜂) → 𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 395
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 396
This theorem is referenced by:  simp-4r  783  ttrcltr  9739  initoeu2  18004  cpmatacl  22617  cpmatmcllem  22619  cpmatmcl  22620  chfacfisf  22755  chfacfisfcpmat  22756  restcld  23075  pthaus  23541  txhaus  23550  xkohaus  23556  alexsubALTlem4  23953  ustuqtop3  24147  ulmcau  26330  2sqreulem1  27378  2sqreunnlem1  27381  clwlkclwwlklem2  29809  rhmimaidl  33148  qsidomlem1  33168  qsdrngi  33206  dimkerim  33321  fedgmul  33325  locfinreflem  33441  cmpcref  33451  pstmxmet  33498  sigapildsys  33781  ldgenpisyslem1  33782  signstfvneq0  34204  nn0prpwlem  35806  matunitlindflem1  37089  matunitlindflem2  37090  poimirlem29  37122  heicant  37128  mblfinlem3  37132  mblfinlem4  37133  itg2addnclem2  37145  itg2gt0cn  37148  ftc1cnnc  37165  sstotbnd2  37247  pell1234qrdich  42281  jm2.26lem3  42422  cvgdvgrat  43750  limsupgtlem  45165  limsupub2  45200  xlimmnfv  45222  icccncfext  45275  fourierdlem34  45529  fourierdlem87  45581  etransclem35  45657  smfaddlem1  46151  sfprmdvdsmersenne  46943  sbgoldbwt  47117  bgoldbtbnd  47149  isuspgrim0  47170  ply1mulgsumlem2  47455  nn0sumshdiglemA  47692
  Copyright terms: Public domain W3C validator