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 715 . 2 ((𝜑 ∧ (𝜏𝜒)) → 𝜃)
323adantr1 1170 1 ((𝜑 ∧ (𝜓𝜏𝜒)) → 𝜃)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 397  w3a 1088
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 206  df-an 398  df-3an 1090
This theorem is referenced by:  simpr3  1197  simpr3l  1235  simpr3r  1236  simpr31  1264  simpr32  1265  simpr33  1266  fpr2g  7165  frfi  9238  ressress  17137  funcestrcsetclem9  18044  funcsetcestrclem9  18059  latjjdir  18389  grprcan  18792  grpsubrcan  18836  grpaddsubass  18845  mhmmnd  18877  zntoslem  20986  ipdir  21066  ipass  21072  qustgpopn  23494  extwwlkfab  29345  grpomuldivass  29532  nvmdi  29639  dmdsl3  31306  dvrcan5  32127  imaslmod  32199  idlsrgmnd  32311  esum2d  32756  voliune  32892  btwnconn1lem7  34731  poimirlem4  36132  cvrnbtwn4  37791  paddasslem14  38346  paddasslem17  38349  paddss  38358  pmod1i  38361  cdleme1  38740  cdleme2  38741  xlimbr  44158  sbgoldbst  46060  funcringcsetcALTV2lem9  46432  funcringcsetclem9ALTV  46455
  Copyright terms: Public domain W3C validator