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

Theorem ad4antlr 733
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 730 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 207  df-an 396
This theorem is referenced by:  simp-4r  784  ttrcltr  9756  initoeu2  18061  cpmatacl  22722  cpmatmcllem  22724  cpmatmcl  22725  chfacfisf  22860  chfacfisfcpmat  22861  restcld  23180  pthaus  23646  txhaus  23655  xkohaus  23661  alexsubALTlem4  24058  ustuqtop3  24252  ulmcau  26438  2sqreulem1  27490  2sqreunnlem1  27493  clwlkclwwlklem2  30019  gsumwun  33068  rhmimaidl  33460  qsidomlem1  33480  qsdrngi  33523  pidufd  33571  dimkerim  33678  fedgmul  33682  locfinreflem  33839  cmpcref  33849  pstmxmet  33896  sigapildsys  34163  ldgenpisyslem1  34164  signstfvneq0  34587  nn0prpwlem  36323  matunitlindflem1  37623  matunitlindflem2  37624  poimirlem29  37656  heicant  37662  mblfinlem3  37666  mblfinlem4  37667  itg2addnclem2  37679  itg2gt0cn  37682  ftc1cnnc  37699  sstotbnd2  37781  pell1234qrdich  42872  jm2.26lem3  43013  cvgdvgrat  44332  limsupgtlem  45792  limsupub2  45827  xlimmnfv  45849  icccncfext  45902  fourierdlem34  46156  fourierdlem87  46208  etransclem35  46284  smfaddlem1  46778  sfprmdvdsmersenne  47590  sbgoldbwt  47764  bgoldbtbnd  47796  isuspgrim0  47872  ply1mulgsumlem2  48304  nn0sumshdiglemA  48540
  Copyright terms: Public domain W3C validator