Theorem 3adant3r2 1202

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  plttr  18507  latjlej2  18621  latmlem1  18636  latmlem2  18637  latledi  18644  latmlej11  18645  latmlej12  18646  ipopos  18703  grppnpcan2  19237  mulgsubdir  19317  imasrng  20392  imasring  20553  isdomn4  20960  zntoslem  21855  mettri2  24653  mettri  24664  xmetrtri  24667  xmetrtri2  24668  metrtri  24669  ablomuldiv  31147  ablonnncan1  31152  nvmdi  31243  dipdi  31438  dipassr  31441  dipsubdir  31443  dipsubdi  31444  btwncomim  36758  cgr3tr4  36797  cgr3rflx  36799  colinbtwnle  36863  rngosubdi  38859  rngosubdir  38860  dmncan1  38990  dmncan2  38991  omlfh1N  40295  omlfh3N  40296  cvrnbtwn3  40313  cvrnbtwn4  40316  cvrcmp2  40321  hlatjrot  40410  cvrat3  40479  lplnribN  40588  ltrn2ateq  41217  dvalveclem  42062  mendlmod  44175  idomcanr  49414