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

Theorem adantl3r 750
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 715 . 2 (((𝜑𝜂) ∧ 𝜓) → (𝜑𝜓))
3 adantl3r.1 . 2 ((((𝜑𝜓) ∧ 𝜒) ∧ 𝜃) → 𝜏)
42, 3sylanl1 680 1 (((((𝜑𝜂) ∧ 𝜓) ∧ 𝜒) ∧ 𝜃) → 𝜏)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 395
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 207  df-an 396
This theorem is referenced by:  adantl4r  755  iscgrglt  28522  legov  28593  dfcgra2  28838  suppovss  32690  cyc3genpm  33172  elrgspnlem4  33249  rhmimaidl  33460  fedgmul  33682  zarclsun  33869  omssubadd  34302  circlemeth  34655  poimirlem29  37656  adantlllr  45044  supxrge  45349  xrralrecnnle  45394  rexabslelem  45429  limclner  45666  xlimmnfvlem2  45848  xlimmnfv  45849  xlimpnfvlem2  45852  xlimpnfv  45853  climxlim2lem  45860  icccncfext  45902  fourierdlem64  46185  fourierdlem73  46194  etransclem35  46284  sge0tsms  46395  hoicvr  46563  hspmbllem2  46642  smflimlem2  46787  smflimlem4  46789
  Copyright terms: Public domain W3C validator