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

Theorem adantl3r 746
Description: Deduction adding 1 conjunct to antecedent. (Contributed by Alan Sare, 17-Oct-2017.)
Hypothesis
Ref Expression
adantl3r.1 ((((𝜑𝜓) ∧ 𝜒) ∧ 𝜃) → 𝜏)
Assertion
Ref Expression
adantl3r (((((𝜑𝜂) ∧ 𝜓) ∧ 𝜒) ∧ 𝜃) → 𝜏)

Proof of Theorem adantl3r
StepHypRef Expression
1 id 22 . . 3 ((𝜑𝜓) → (𝜑𝜓))
21adantlr 711 . 2 (((𝜑𝜂) ∧ 𝜓) → (𝜑𝜓))
3 adantl3r.1 . 2 ((((𝜑𝜓) ∧ 𝜒) ∧ 𝜃) → 𝜏)
42, 3sylanl1 676 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:  adantl4r  751  iscgrglt  25987  legov  26058  dfcgra2  26303  suppovss  30121  cyc3genpm  30437  fedgmul  30636  omssubadd  31180  circlemeth  31533  poimirlem29  34477  adantlllr  40861  supxrge  41172  xrralrecnnle  41219  rexabslelem  41259  limclner  41499  xlimmnfvlem2  41681  xlimmnfv  41682  xlimpnfvlem2  41685  xlimpnfv  41686  climxlim2lem  41693  icccncfext  41737  fourierdlem64  42023  fourierdlem73  42032  etransclem35  42122  sge0tsms  42230  hoicvr  42398  hspmbllem2  42477  smflimlem2  42616  smflimlem4  42618
  Copyright terms: Public domain W3C validator