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

Theorem ad4antlr 773
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 473 . 2 ((𝜒𝜑) → 𝜓)
32ad3antrrr 768 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 197  df-an 385
This theorem is referenced by:  ad5antlrOLD  778  initoeu2  16867  cpmatacl  20723  cpmatmcllem  20725  cpmatmcl  20726  chfacfisf  20861  chfacfisfcpmat  20862  restcld  21178  pthaus  21643  txhaus  21652  xkohaus  21658  alexsubALTlem4  22055  ustuqtop3  22248  ulmcau  24348  clwlkclwwlklem2  27123  locfinreflem  30216  cmpcref  30226  pstmxmet  30249  sigapildsys  30534  ldgenpisyslem1  30535  nn0prpwlem  32623  matunitlindflem1  33718  matunitlindflem2  33719  poimirlem29  33751  heicant  33757  mblfinlem3  33761  mblfinlem4  33762  itg2addnclem2  33775  itg2gt0cn  33778  ftc1cnnc  33797  sstotbnd2  33886  pell1234qrdich  37927  jm2.26lem3  38070  cvgdvgrat  39014  limsupgtlem  40512  xlimmnfv  40563  icccncfext  40603  fourierdlem34  40861  fourierdlem87  40913  etransclem35  40989  smfaddlem1  41477  sfprmdvdsmersenne  42030  sbgoldbwt  42175  bgoldbtbnd  42207  ply1mulgsumlem2  42685  nn0sumshdiglemA  42923
  Copyright terms: Public domain W3C validator