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

Syntax hints:   → wi 4   ∧ wa 395   ∧ 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 207  df-an 396  df-3an 1088

This theorem is referenced by:  plttr  18308  latjlej2  18420  latmlem1  18435  latmlem2  18436  latledi  18443  latmlej11  18444  latmlej12  18445  ipopos  18502  grppnpcan2  18973  mulgsubdir  19053  imasrng  20093  imasring  20246  isdomn4  20632  zntoslem  21473  mettri2  24236  mettri  24247  xmetrtri  24250  xmetrtri2  24251  metrtri  24252  ablomuldiv  30488  ablonnncan1  30493  nvmdi  30584  dipdi  30779  dipassr  30782  dipsubdir  30784  dipsubdi  30785  btwncomim  36008  cgr3tr4  36047  cgr3rflx  36049  colinbtwnle  36113  rngosubdi  37946  rngosubdir  37947  dmncan1  38077  dmncan2  38078  omlfh1N  39258  omlfh3N  39259  cvrnbtwn3  39276  cvrnbtwn4  39279  cvrcmp2  39284  hlatjrot  39373  cvrat3  39443  lplnribN  39552  ltrn2ateq  40181  dvalveclem  41026  mendlmod  43185