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

Theorem 3ad2antr3 1191
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 716 . 2 ((𝜑 ∧ (𝜏𝜒)) → 𝜃)
323adantr1 1170 1 ((𝜑 ∧ (𝜓𝜏𝜒)) → 𝜃)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 395  w3a 1087
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 207  df-an 396  df-3an 1089
This theorem is referenced by:  simpr3  1197  simpr3l  1235  simpr3r  1236  simpr31  1264  simpr32  1265  simpr33  1266  fpr2g  7231  frfi  9321  ressress  17293  funcestrcsetclem9  18193  funcsetcestrclem9  18208  latjjdir  18537  grprcan  18991  grpsubrcan  19039  grpaddsubass  19048  mhmmnd  19082  zntoslem  21575  ipdir  21657  ipass  21663  qustgpopn  24128  extwwlkfab  30371  grpomuldivass  30560  nvmdi  30667  dmdsl3  32334  dvrcan5  33240  imaslmod  33381  idlsrgmnd  33542  esum2d  34094  voliune  34230  btwnconn1lem7  36094  poimirlem4  37631  cvrnbtwn4  39280  paddasslem14  39835  paddasslem17  39838  paddss  39847  pmod1i  39850  cdleme1  40229  cdleme2  40230  xlimbr  45842  sbgoldbst  47765  funcringcsetcALTV2lem9  48214  funcringcsetclem9ALTV  48237
  Copyright terms: Public domain W3C validator