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

Theorem 3ad2antr3 1205
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 695 . 2 ((𝜑 ∧ (𝜏𝜒)) → 𝜃)
323adantr1 1174 1 ((𝜑 ∧ (𝜓𝜏𝜒)) → 𝜃)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 382  w3a 1071
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 383  df-3an 1073
This theorem is referenced by:  simpr3  1237  simpr3l  1298  simpr3r  1300  simpr31  1344  simpr32  1346  simpr33  1348  fpr2g  6619  frfi  8361  ressress  16146  funcestrcsetclem9  16996  funcsetcestrclem9  17011  latjjdir  17312  grprcan  17663  grpsubrcan  17704  grpaddsubass  17713  mhmmnd  17745  zntoslem  20120  ipdir  20201  ipass  20207  qustgpopn  22143  extwwlkfab  27538  grpomuldivass  27735  nvmdi  27843  dmdsl3  29514  dvrcan5  30133  esum2d  30495  voliune  30632  btwnconn1lem7  32537  poimirlem4  33746  cvrnbtwn4  35088  paddasslem14  35641  paddasslem17  35644  paddss  35653  pmod1i  35656  cdleme1  36036  cdleme2  36037  xlimbr  40571  sbgoldbst  42194  funcringcsetcALTV2lem9  42572  funcringcsetclem9ALTV  42595
  Copyright terms: Public domain W3C validator