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

Theorem 3ad2antr2 1190
Description: Deduction adding conjuncts to antecedent. (Contributed by NM, 27-Dec-2007.)
Hypothesis
Ref Expression
3ad2antl.1 ((𝜑𝜒) → 𝜃)
Assertion
Ref Expression
3ad2antr2 ((𝜑 ∧ (𝜓𝜒𝜏)) → 𝜃)

Proof of Theorem 3ad2antr2
StepHypRef Expression
1 3ad2antl.1 . . 3 ((𝜑𝜒) → 𝜃)
21adantrl 716 . 2 ((𝜑 ∧ (𝜓𝜒)) → 𝜃)
323adantr3 1172 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:  simpr2  1196  simpr2l  1233  simpr2r  1234  simpr21  1261  simpr22  1262  simpr23  1263  wereu  5681  axdc4lem  10495  ioc0  13434  funcestrcsetclem9  18193  funcsetcestrclem9  18208  grpsubadd  19046  zntoslem  21575  mdsl3  32335  dvrcan5  33240  idlsrgmnd  33542  prv1n  35436  brofs2  36078  brifs2  36079  poimirlem28  37655  ftc1anc  37708  frinfm  37742  welb  37743  fdc  37752  unichnidl  38038  cvrnbtwn2  39276  islpln2a  39550  paddss1  39819  paddss2  39820  paddasslem17  39838  tendospass  41021  funcringcsetcALTV2lem9  48214  funcringcsetclem9ALTV  48237  ldepsprlem  48389
  Copyright terms: Public domain W3C validator