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

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

Proof of Theorem 3adant3r2
StepHypRef Expression
1 3exp.1 . . 3 ((𝜑𝜓𝜒) → 𝜃)
213expb 1285 . 2 ((𝜑 ∧ (𝜓𝜒)) → 𝜃)
323adantr2 1241 1 ((𝜑 ∧ (𝜓𝜏𝜒)) → 𝜃)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 383  w3a 1054
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 197  df-an 385  df-3an 1056
This theorem is referenced by:  plttr  17017  latjlej2  17113  latmlem1  17128  latmlem2  17129  latledi  17136  latmlej11  17137  latmlej12  17138  ipopos  17207  grppnpcan2  17556  mulgsubdir  17629  imasring  18665  zntoslem  19953  mettri2  22193  mettri  22204  xmetrtri  22207  xmetrtri2  22208  metrtri  22209  ablomuldiv  27534  ablonnncan1  27540  nvmdi  27631  dipdi  27826  dipassr  27829  dipsubdir  27831  dipsubdi  27832  btwncomim  32245  cgr3tr4  32284  cgr3rflx  32286  colinbtwnle  32350  rngosubdi  33874  rngosubdir  33875  dmncan1  34005  dmncan2  34006  omlfh1N  34863  omlfh3N  34864  cvrnbtwn3  34881  cvrnbtwn4  34884  cvrcmp2  34889  hlatjrot  34977  cvrat3  35046  lplnribN  35155  ltrn2ateq  35785  dvalveclem  36631  mendlmod  38080
  Copyright terms: Public domain W3C validator