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

Theorem 3adant3r2 1163
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 1100 . 2 ((𝜑 ∧ (𝜓𝜒)) → 𝜃)
323adantr2 1150 1 ((𝜑 ∧ (𝜓𝜏𝜒)) → 𝜃)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 387  w3a 1068
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 199  df-an 388  df-3an 1070
This theorem is referenced by:  plttr  17432  latjlej2  17528  latmlem1  17543  latmlem2  17544  latledi  17551  latmlej11  17552  latmlej12  17553  ipopos  17622  grppnpcan2  17974  mulgsubdir  18045  imasring  19086  zntoslem  20399  mettri2  22648  mettri  22659  xmetrtri  22662  xmetrtri2  22663  metrtri  22664  ablomuldiv  28100  ablonnncan1  28105  nvmdi  28196  dipdi  28391  dipassr  28394  dipsubdir  28396  dipsubdi  28397  btwncomim  32995  cgr3tr4  33034  cgr3rflx  33036  colinbtwnle  33100  rngosubdi  34665  rngosubdir  34666  dmncan1  34796  dmncan2  34797  omlfh1N  35839  omlfh3N  35840  cvrnbtwn3  35857  cvrnbtwn4  35860  cvrcmp2  35865  hlatjrot  35954  cvrat3  36023  lplnribN  36132  ltrn2ateq  36761  dvalveclem  37606  mendlmod  39189
  Copyright terms: Public domain W3C validator