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

Theorem 3adantr2 1166
 Description: Deduction adding a conjunct to antecedent. (Contributed by NM, 27-Apr-2005.)
Hypothesis
Ref Expression
3adantr.1 ((𝜑 ∧ (𝜓𝜒)) → 𝜃)
Assertion
Ref Expression
3adantr2 ((𝜑 ∧ (𝜓𝜏𝜒)) → 𝜃)

Proof of Theorem 3adantr2
StepHypRef Expression
1 3simpb 1145 . 2 ((𝜓𝜏𝜒) → (𝜓𝜒))
2 3adantr.1 . 2 ((𝜑 ∧ (𝜓𝜒)) → 𝜃)
31, 2sylan2 594 1 ((𝜑 ∧ (𝜓𝜏𝜒)) → 𝜃)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 398   ∧ w3a 1083 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 209  df-an 399  df-3an 1085 This theorem is referenced by:  3adant3r2  1179  po3nr  5483  funcnvqp  6413  sornom  9693  axdclem2  9936  fzadd2  12936  issubc3  17113  funcestrcsetclem9  17392  funcsetcestrclem9  17407  pgpfi  18724  imasring  19363  prdslmodd  19735  icoopnst  23537  iocopnst  23538  axcontlem4  26747  nvmdi  28419  mdsl3  30087  elicc3  33660  iscringd  35270  erngdvlem3  38120  erngdvlem3-rN  38128  dvalveclem  38155  dvhlveclem  38238  dvmptfprodlem  42221  smflimlem4  43043  funcringcsetcALTV2lem9  44308  funcringcsetclem9ALTV  44331
 Copyright terms: Public domain W3C validator