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

Theorem adantl3r 747
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 712 . 2 (((𝜑𝜂) ∧ 𝜓) → (𝜑𝜓))
3 adantl3r.1 . 2 ((((𝜑𝜓) ∧ 𝜒) ∧ 𝜃) → 𝜏)
42, 3sylanl1 677 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:  adantl4r  752  iscgrglt  26875  legov  26946  dfcgra2  27191  suppovss  31017  cyc3genpm  31419  rhmimaidl  31609  fedgmul  31712  zarclsun  31820  omssubadd  32267  circlemeth  32620  poimirlem29  35806  adantlllr  42583  supxrge  42877  xrralrecnnle  42922  rexabslelem  42958  limclner  43192  xlimmnfvlem2  43374  xlimmnfv  43375  xlimpnfvlem2  43378  xlimpnfv  43379  climxlim2lem  43386  icccncfext  43428  fourierdlem64  43711  fourierdlem73  43720  etransclem35  43810  sge0tsms  43918  hoicvr  44086  hspmbllem2  44165  smflimlem2  44307  smflimlem4  44309
  Copyright terms: Public domain W3C validator