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

Theorem adantl3r 803
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 adantl3r.1 . . . 4 ((((𝜑𝜓) ∧ 𝜒) ∧ 𝜃) → 𝜏)
21ex 449 . . 3 (((𝜑𝜓) ∧ 𝜒) → (𝜃𝜏))
32adantllr 757 . 2 ((((𝜑𝜂) ∧ 𝜓) ∧ 𝜒) → (𝜃𝜏))
43imp 444 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:  adantl4r  804  ad5ant1345  1473  iscgrglt  25608  legov  25679  dfcgra2  25920  omssubadd  30671  circlemeth  31027  poimirlem29  33751  adantlllr  39698  supxrge  40052  xrralrecnnle  40100  rexabslelem  40143  limclner  40386  xlimmnfvlem2  40562  xlimmnfv  40563  xlimpnfvlem2  40566  xlimpnfv  40567  climxlim2lem  40574  icccncfext  40603  fourierdlem64  40890  fourierdlem73  40899  etransclem35  40989  sge0tsms  41100  hoicvr  41268  hspmbllem2  41347  smflimlem2  41486  smflimlem4  41488
  Copyright terms: Public domain W3C validator