Theorem 3adant3r2 1182

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 1119	. 2 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃)
3	2	3adantr2 1169	1 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜏 ∧ 𝜒)) → 𝜃)

Syntax hints:   → wi 4   ∧ wa 396   ∧ w3a 1086

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 206  df-an 397  df-3an 1088

This theorem is referenced by:  plttr  18071  latjlej2  18183  latmlem1  18198  latmlem2  18199  latledi  18206  latmlej11  18207  latmlej12  18208  ipopos  18265  grppnpcan2  18680  mulgsubdir  18754  imasring  19869  zntoslem  20775  mettri2  23505  mettri  23516  xmetrtri  23519  xmetrtri2  23520  metrtri  23521  ablomuldiv  28923  ablonnncan1  28928  nvmdi  29019  dipdi  29214  dipassr  29217  dipsubdir  29219  dipsubdi  29220  btwncomim  34324  cgr3tr4  34363  cgr3rflx  34365  colinbtwnle  34429  rngosubdi  36112  rngosubdir  36113  dmncan1  36243  dmncan2  36244  omlfh1N  37281  omlfh3N  37282  cvrnbtwn3  37299  cvrnbtwn4  37302  cvrcmp2  37307  hlatjrot  37396  cvrat3  37465  lplnribN  37574  ltrn2ateq  38203  dvalveclem  39048  isdomn4  40181  mendlmod  41027