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

Theorem 3ad2antr3 1206
Description: Deduction adding conjuncts to antecedent. (Contributed by NM, 30-Dec-2007.)
Hypothesis
Ref Expression
3ad2antl.1 ((𝜑𝜒) → 𝜃)
Assertion
Ref Expression
3ad2antr3 ((𝜑 ∧ (𝜓𝜏𝜒)) → 𝜃)

Proof of Theorem 3ad2antr3
StepHypRef Expression
1 3ad2antl.1 . . 3 ((𝜑𝜒) → 𝜃)
21adantrl 754 . 2 ((𝜑 ∧ (𝜏𝜒)) → 𝜃)
323adantr1 1175 1 ((𝜑 ∧ (𝜓𝜏𝜒)) → 𝜃)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 383  w3a 1072
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  df-3an 1074
This theorem is referenced by:  simpr3  1238  simpr3l  1299  simpr3r  1301  simpr31  1345  simpr32  1347  simpr33  1349  fpr2g  6640  frfi  8372  ressress  16160  funcestrcsetclem9  17009  funcsetcestrclem9  17024  latjjdir  17325  grprcan  17676  grpsubrcan  17717  grpaddsubass  17726  mhmmnd  17758  zntoslem  20127  ipdir  20206  ipass  20212  qustgpopn  22144  extwwlkfab  27532  grpomuldivass  27725  nvmdi  27833  dmdsl3  29504  dvrcan5  30123  esum2d  30485  voliune  30622  btwnconn1lem7  32527  poimirlem4  33744  cvrnbtwn4  35087  paddasslem14  35640  paddasslem17  35643  paddss  35652  pmod1i  35655  cdleme1  36035  cdleme2  36036  xlimbr  40574  sbgoldbst  42194  funcringcsetcALTV2lem9  42572  funcringcsetclem9ALTV  42595
  Copyright terms: Public domain W3C validator