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  18246  latjlej2  18360  latmlem1  18375  latmlem2  18376  latledi  18383  latmlej11  18384  latmlej12  18385  ipopos  18442  grppnpcan2  18913  mulgsubdir  18993  imasrng  20062  imasring  20215  isdomn4  20601  zntoslem  21463  mettri2  24227  mettri  24238  xmetrtri  24241  xmetrtri2  24242  metrtri  24243  ablomuldiv  30496  ablonnncan1  30501  nvmdi  30592  dipdi  30787  dipassr  30790  dipsubdir  30792  dipsubdi  30793  btwncomim  35987  cgr3tr4  36026  cgr3rflx  36028  colinbtwnle  36092  rngosubdi  37925  rngosubdir  37926  dmncan1  38056  dmncan2  38057  omlfh1N  39237  omlfh3N  39238  cvrnbtwn3  39255  cvrnbtwn4  39258  cvrcmp2  39263  hlatjrot  39352  cvrat3  39421  lplnribN  39530  ltrn2ateq  40159  dvalveclem  41004  mendlmod  43162