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 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜏 ∧ 𝜒)) → 𝜃)

Syntax hints:   → wi 4   ∧ wa 400   ∧ w3a 1103

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 210  df-an 401  df-3an 1105

This theorem is referenced by:  plttr  18391  latjlej2  18505  latmlem1  18520  latmlem2  18521  latledi  18528  latmlej11  18529  latmlej12  18530  ipopos  18587  grppnpcan2  19095  mulgsubdir  19175  imasrng  20250  imasring  20408  isdomn4  20814  zntoslem  21706  mettri2  24498  mettri  24509  xmetrtri  24512  xmetrtri2  24513  metrtri  24514  ablomuldiv  30904  ablonnncan1  30909  nvmdi  31000  dipdi  31195  dipassr  31198  dipsubdir  31200  dipsubdi  31201  btwncomim  36505  cgr3tr4  36544  cgr3rflx  36546  colinbtwnle  36610  rngosubdi  38596  rngosubdir  38597  dmncan1  38727  dmncan2  38728  omlfh1N  40032  omlfh3N  40033  cvrnbtwn3  40050  cvrnbtwn4  40053  cvrcmp2  40058  hlatjrot  40147  cvrat3  40216  lplnribN  40325  ltrn2ateq  40954  dvalveclem  41799  mendlmod  43916  idomcanr  49113