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

Theorem ad4antlr 729
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 482 . 2 ((𝜒𝜑) → 𝜓)
32ad3antrrr 726 1 (((((𝜒𝜑) ∧ 𝜃) ∧ 𝜏) ∧ 𝜂) → 𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396
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 208  df-an 397
This theorem is referenced by:  simp-4r  780  initoeu2  17264  cpmatacl  21252  cpmatmcllem  21254  cpmatmcl  21255  chfacfisf  21390  chfacfisfcpmat  21391  restcld  21708  pthaus  22174  txhaus  22183  xkohaus  22189  alexsubALTlem4  22586  ustuqtop3  22779  ulmcau  24910  2sqreulem1  25949  2sqreunnlem1  25952  clwlkclwwlklem2  27705  qsidomlem1  30882  dimkerim  30922  fedgmul  30926  locfinreflem  31003  cmpcref  31013  pstmxmet  31036  sigapildsys  31320  ldgenpisyslem1  31321  signstfvneq0  31741  nn0prpwlem  33567  matunitlindflem1  34769  matunitlindflem2  34770  poimirlem29  34802  heicant  34808  mblfinlem3  34812  mblfinlem4  34813  itg2addnclem2  34825  itg2gt0cn  34828  ftc1cnnc  34847  sstotbnd2  34933  pell1234qrdich  39336  jm2.26lem3  39476  cvgdvgrat  40522  limsupgtlem  41934  limsupub2  41969  xlimmnfv  41991  icccncfext  42046  fourierdlem34  42303  fourierdlem87  42355  etransclem35  42431  smfaddlem1  42916  sfprmdvdsmersenne  43645  sbgoldbwt  43819  bgoldbtbnd  43851  ply1mulgsumlem2  44369  nn0sumshdiglemA  44607
  Copyright terms: Public domain W3C validator