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

Theorem 3ad2antr3 1220
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 747 . 2 ((𝜑 ∧ (𝜏𝜒)) → 𝜃)
323adantr1 1212 1 ((𝜑 ∧ (𝜓𝜏𝜒)) → 𝜃)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 382  w3a 1030
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 195  df-an 384  df-3an 1032
This theorem is referenced by:  fpr2g  6357  frfi  8067  ressress  15713  funcestrcsetclem9  16559  funcsetcestrclem9  16574  latjjdir  16875  grprcan  17226  grpsubrcan  17267  grpaddsubass  17276  mhmmnd  17308  zntoslem  19671  ipdir  19750  ipass  19756  qustgpopn  21680  constr3trllem1  25971  wwlkextproplem3  26064  grpomuldivass  26572  nvmdi  26680  dmdsl3  28351  dvrcan5  28917  esum2d  29275  voliune  29412  btwnconn1lem7  31163  poimirlem4  32366  cvrnbtwn4  33367  paddasslem14  33920  paddasslem17  33923  paddss  33932  pmod1i  33935  cdleme1  34315  cdleme2  34316  bgoldbst  39984  funcringcsetcALTV2lem9  41817  funcringcsetclem9ALTV  41840
  Copyright terms: Public domain W3C validator