Theorem 3adant3r2 1200

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

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

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 1103

This theorem is referenced by:  plttr  18395  latjlej2  18509  latmlem1  18524  latmlem2  18525  latledi  18532  latmlej11  18533  latmlej12  18534  ipopos  18591  grppnpcan2  19099  mulgsubdir  19179  imasrng  20254  imasring  20411  isdomn4  20799  zntoslem  21674  mettri2  24466  mettri  24477  xmetrtri  24480  xmetrtri2  24481  metrtri  24482  ablomuldiv  30844  ablonnncan1  30849  nvmdi  30940  dipdi  31135  dipassr  31138  dipsubdir  31140  dipsubdi  31141  btwncomim  36403  cgr3tr4  36442  cgr3rflx  36444  colinbtwnle  36508  rngosubdi  38483  rngosubdir  38484  dmncan1  38614  dmncan2  38615  omlfh1N  39921  omlfh3N  39922  cvrnbtwn3  39939  cvrnbtwn4  39942  cvrcmp2  39947  hlatjrot  40036  cvrat3  40105  lplnribN  40214  ltrn2ateq  40843  dvalveclem  41688  mendlmod  43807