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

Theorem ad4antlr 730
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 727 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 206  df-an 397
This theorem is referenced by:  simp-4r  781  ttrcltr  9573  initoeu2  17828  cpmatacl  21971  cpmatmcllem  21973  cpmatmcl  21974  chfacfisf  22109  chfacfisfcpmat  22110  restcld  22429  pthaus  22895  txhaus  22904  xkohaus  22910  alexsubALTlem4  23307  ustuqtop3  23501  ulmcau  25660  2sqreulem1  26700  2sqreunnlem1  26703  clwlkclwwlklem2  28652  rhmimaidl  31906  qsidomlem1  31925  dimkerim  32006  fedgmul  32010  locfinreflem  32088  cmpcref  32098  pstmxmet  32145  sigapildsys  32428  ldgenpisyslem1  32429  signstfvneq0  32851  nn0prpwlem  34607  matunitlindflem1  35878  matunitlindflem2  35879  poimirlem29  35911  heicant  35917  mblfinlem3  35921  mblfinlem4  35922  itg2addnclem2  35934  itg2gt0cn  35937  ftc1cnnc  35954  sstotbnd2  36037  pell1234qrdich  40945  jm2.26lem3  41086  cvgdvgrat  42252  limsupgtlem  43654  limsupub2  43689  xlimmnfv  43711  icccncfext  43764  fourierdlem34  44018  fourierdlem87  44070  etransclem35  44146  smfaddlem1  44638  sfprmdvdsmersenne  45406  sbgoldbwt  45580  bgoldbtbnd  45612  ply1mulgsumlem2  46079  nn0sumshdiglemA  46316
  Copyright terms: Public domain W3C validator