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

Theorem 3ad2antr3 1182
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 712 . 2 ((𝜑 ∧ (𝜏𝜒)) → 𝜃)
323adantr1 1161 1 ((𝜑 ∧ (𝜓𝜏𝜒)) → 𝜃)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396  w3a 1079
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 208  df-an 397  df-3an 1081
This theorem is referenced by:  simpr3  1188  simpr3l  1226  simpr3r  1227  simpr31  1255  simpr32  1256  simpr33  1257  fpr2g  6965  frfi  8751  ressress  16550  funcestrcsetclem9  17386  funcsetcestrclem9  17401  latjjdir  17702  grprcan  18075  grpsubrcan  18118  grpaddsubass  18127  mhmmnd  18159  zntoslem  20631  ipdir  20711  ipass  20717  qustgpopn  22655  extwwlkfab  28058  grpomuldivass  28245  nvmdi  28352  dmdsl3  30019  dvrcan5  30791  imaslmod  30849  esum2d  31251  voliune  31387  btwnconn1lem7  33451  poimirlem4  34777  cvrnbtwn4  36295  paddasslem14  36849  paddasslem17  36852  paddss  36861  pmod1i  36864  cdleme1  37243  cdleme2  37244  xlimbr  41984  sbgoldbst  43820  funcringcsetcALTV2lem9  44243  funcringcsetclem9ALTV  44266
  Copyright terms: Public domain W3C validator