Theorem 3adant3r2 1181

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

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1085

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 206  df-an 396  df-3an 1087

This theorem is referenced by:  plttr  18328  latjlej2  18440  latmlem1  18455  latmlem2  18456  latledi  18463  latmlej11  18464  latmlej12  18465  ipopos  18522  grppnpcan2  18984  mulgsubdir  19063  imasrng  20111  imasring  20260  isdomn4  21244  zntoslem  21484  mettri2  24241  mettri  24252  xmetrtri  24255  xmetrtri2  24256  metrtri  24257  ablomuldiv  30356  ablonnncan1  30361  nvmdi  30452  dipdi  30647  dipassr  30650  dipsubdir  30652  dipsubdi  30653  btwncomim  35604  cgr3tr4  35643  cgr3rflx  35645  colinbtwnle  35709  rngosubdi  37413  rngosubdir  37414  dmncan1  37544  dmncan2  37545  omlfh1N  38725  omlfh3N  38726  cvrnbtwn3  38743  cvrnbtwn4  38746  cvrcmp2  38751  hlatjrot  38840  cvrat3  38910  lplnribN  39019  ltrn2ateq  39648  dvalveclem  40493  mendlmod  42608