Theorem 3adant3r2 1266

Description: Deduction adding a conjunct to antecedent. (Contributed by NM, 17-Feb-2008.)

Hypothesis

Ref	Expression
3exp.1	⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)

Assertion

Ref	Expression
3adant3r2	⊢ ((𝜑 ∧ (𝜓 ∧ 𝜏 ∧ 𝜒)) → 𝜃)

Proof of Theorem 3adant3r2

Step	Hyp	Ref	Expression
1		3exp.1	. . 3 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)
2	1	3expb 1257	. 2 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃)
3	2	3adantr2 1213	1 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜏 ∧ 𝜒)) → 𝜃)

Syntax hints:   → wi 4   ∧ wa 382   ∧ w3a 1030

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 195  df-an 384  df-3an 1032

This theorem is referenced by:  plttr  16739  latjlej2  16835  latmlem1  16850  latmlem2  16851  latledi  16858  latmlej11  16859  latmlej12  16860  ipopos  16929  grppnpcan2  17278  mulgsubdir  17351  imasring  18388  zntoslem  19669  mettri2  21897  mettri  21908  xmetrtri  21911  xmetrtri2  21912  metrtri  21913  grpopnpcan2  26548  grponnncan2  26549  ablomuldiv  26559  ablonnncan1  26565  nvmdi  26675  dipdi  26888  dipassr  26891  dipsubdir  26893  dipsubdi  26894  btwncomim  31096  cgr3tr4  31135  cgr3rflx  31137  colinbtwnle  31201  rngosubdi  32717  rngosubdir  32718  dmncan1  32848  dmncan2  32849  omlfh1N  33366  omlfh3N  33367  cvrnbtwn3  33384  cvrnbtwn4  33387  cvrcmp2  33392  hlatjrot  33480  cvrat3  33549  lplnribN  33658  ltrn2ateq  34288  dvalveclem  35135  mendlmod  36585