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

Theorem 3adant3r2 1199
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 1114 . 2 ((𝜑 ∧ (𝜓𝜒)) → 𝜃)
323adantr2 1176 1 ((𝜑 ∧ (𝜓𝜏𝜒)) → 𝜃)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 383  w3a 1072
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 1074
This theorem is referenced by:  plttr  17192  latjlej2  17288  latmlem1  17303  latmlem2  17304  latledi  17311  latmlej11  17312  latmlej12  17313  ipopos  17382  grppnpcan2  17731  mulgsubdir  17804  imasring  18840  zntoslem  20128  mettri2  22368  mettri  22379  xmetrtri  22382  xmetrtri2  22383  metrtri  22384  ablomuldiv  27737  ablonnncan1  27743  nvmdi  27834  dipdi  28029  dipassr  28032  dipsubdir  28034  dipsubdi  28035  btwncomim  32448  cgr3tr4  32487  cgr3rflx  32489  colinbtwnle  32553  rngosubdi  34076  rngosubdir  34077  dmncan1  34207  dmncan2  34208  omlfh1N  35067  omlfh3N  35068  cvrnbtwn3  35085  cvrnbtwn4  35088  cvrcmp2  35093  hlatjrot  35181  cvrat3  35250  lplnribN  35359  ltrn2ateq  35989  dvalveclem  36835  mendlmod  38284
  Copyright terms: Public domain W3C validator