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

Theorem ad4antlr 771
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 766 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  776  initoeu2  16713  cpmatacl  20569  cpmatmcllem  20571  cpmatmcl  20572  chfacfisf  20707  chfacfisfcpmat  20708  restcld  21024  pthaus  21489  txhaus  21498  xkohaus  21504  alexsubALTlem4  21901  ustuqtop3  22094  ulmcau  24194  clwlkclwwlklem2  26966  locfinreflem  30035  cmpcref  30045  pstmxmet  30068  sigapildsys  30353  ldgenpisyslem1  30354  nn0prpwlem  32442  matunitlindflem1  33535  matunitlindflem2  33536  poimirlem29  33568  heicant  33574  mblfinlem3  33578  mblfinlem4  33579  itg2addnclem2  33592  itg2gt0cn  33595  ftc1cnnc  33614  sstotbnd2  33703  pell1234qrdich  37742  jm2.26lem3  37885  cvgdvgrat  38829  limsupgtlem  40327  xlimmnfv  40378  icccncfext  40418  fourierdlem34  40676  fourierdlem87  40728  etransclem35  40804  smfaddlem1  41292  sfprmdvdsmersenne  41845  sbgoldbwt  41990  bgoldbtbnd  42022  ply1mulgsumlem2  42500  nn0sumshdiglemA  42738
  Copyright terms: Public domain W3C validator