Theorem 3adant3r2 1202

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  plttr  18523  latjlej2  18637  latmlem1  18652  latmlem2  18653  latledi  18660  latmlej11  18661  latmlej12  18662  ipopos  18719  grppnpcan2  19253  mulgsubdir  19333  imasrng  20408  imasring  20569  isdomn4  20976  zntoslem  21871  mettri2  24669  mettri  24680  xmetrtri  24683  xmetrtri2  24684  metrtri  24685  ablomuldiv  31163  ablonnncan1  31168  nvmdi  31259  dipdi  31454  dipassr  31457  dipsubdir  31459  dipsubdi  31460  btwncomim  36874  cgr3tr4  36913  cgr3rflx  36915  colinbtwnle  36979  rngosubdi  38988  rngosubdir  38989  dmncan1  39119  dmncan2  39120  omlfh1N  40424  omlfh3N  40425  cvrnbtwn3  40442  cvrnbtwn4  40445  cvrcmp2  40450  hlatjrot  40539  cvrat3  40608  lplnribN  40717  ltrn2ateq  41346  dvalveclem  42191  mendlmod  44300  idomcanr  49553