Theorem 3adant3r2 1184

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

Step	Hyp	Ref	Expression
1		ad4ant3.1	. . 3 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)
2	1	3expb 1121	. 2 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃)
3	2	3adantr2 1171	1 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜏 ∧ 𝜒)) → 𝜃)

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1087

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 207  df-an 396  df-3an 1089

This theorem is referenced by:  plttr  18387  latjlej2  18499  latmlem1  18514  latmlem2  18515  latledi  18522  latmlej11  18523  latmlej12  18524  ipopos  18581  grppnpcan2  19052  mulgsubdir  19132  imasrng  20174  imasring  20327  isdomn4  20716  zntoslem  21575  mettri2  24351  mettri  24362  xmetrtri  24365  xmetrtri2  24366  metrtri  24367  ablomuldiv  30571  ablonnncan1  30576  nvmdi  30667  dipdi  30862  dipassr  30865  dipsubdir  30867  dipsubdi  30868  btwncomim  36014  cgr3tr4  36053  cgr3rflx  36055  colinbtwnle  36119  rngosubdi  37952  rngosubdir  37953  dmncan1  38083  dmncan2  38084  omlfh1N  39259  omlfh3N  39260  cvrnbtwn3  39277  cvrnbtwn4  39280  cvrcmp2  39285  hlatjrot  39374  cvrat3  39444  lplnribN  39553  ltrn2ateq  40182  dvalveclem  41027  mendlmod  43201