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  18350  latjlej2  18462  latmlem1  18477  latmlem2  18478  latledi  18485  latmlej11  18486  latmlej12  18487  ipopos  18544  grppnpcan2  19015  mulgsubdir  19095  imasrng  20135  imasring  20288  isdomn4  20674  zntoslem  21515  mettri2  24278  mettri  24289  xmetrtri  24292  xmetrtri2  24293  metrtri  24294  ablomuldiv  30479  ablonnncan1  30484  nvmdi  30575  dipdi  30770  dipassr  30773  dipsubdir  30775  dipsubdi  30776  btwncomim  35977  cgr3tr4  36016  cgr3rflx  36018  colinbtwnle  36082  rngosubdi  37915  rngosubdir  37916  dmncan1  38046  dmncan2  38047  omlfh1N  39222  omlfh3N  39223  cvrnbtwn3  39240  cvrnbtwn4  39243  cvrcmp2  39248  hlatjrot  39337  cvrat3  39407  lplnribN  39516  ltrn2ateq  40145  dvalveclem  40990  mendlmod  43160