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

Theorem 3adant3r2 1180
Description: Deduction adding a conjunct to antecedent. (Contributed by NM, 17-Feb-2008.)
Hypothesis
Ref Expression
ad4ant3.1 ((𝜑𝜓𝜒) → 𝜃)
Assertion
Ref Expression
3adant3r2 ((𝜑 ∧ (𝜓𝜏𝜒)) → 𝜃)

Proof of Theorem 3adant3r2
StepHypRef Expression
1 ad4ant3.1 . . 3 ((𝜑𝜓𝜒) → 𝜃)
213expb 1117 . 2 ((𝜑 ∧ (𝜓𝜒)) → 𝜃)
323adantr2 1167 1 ((𝜑 ∧ (𝜓𝜏𝜒)) → 𝜃)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 399  w3a 1084
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 210  df-an 400  df-3an 1086
This theorem is referenced by:  plttr  17572  latjlej2  17668  latmlem1  17683  latmlem2  17684  latledi  17691  latmlej11  17692  latmlej12  17693  ipopos  17762  grppnpcan2  18185  mulgsubdir  18259  imasring  19365  zntoslem  20248  mettri2  22948  mettri  22959  xmetrtri  22962  xmetrtri2  22963  metrtri  22964  ablomuldiv  28335  ablonnncan1  28340  nvmdi  28431  dipdi  28626  dipassr  28629  dipsubdir  28631  dipsubdi  28632  btwncomim  33587  cgr3tr4  33626  cgr3rflx  33628  colinbtwnle  33692  rngosubdi  35383  rngosubdir  35384  dmncan1  35514  dmncan2  35515  omlfh1N  36554  omlfh3N  36555  cvrnbtwn3  36572  cvrnbtwn4  36575  cvrcmp2  36580  hlatjrot  36669  cvrat3  36738  lplnribN  36847  ltrn2ateq  37476  dvalveclem  38321  mendlmod  40135
  Copyright terms: Public domain W3C validator