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  18564  latjlej2  18678  latmlem1  18693  latmlem2  18694  latledi  18701  latmlej11  18702  latmlej12  18703  ipopos  18760  grppnpcan2  19294  mulgsubdir  19374  imasrng  20450  imasring  20611  isdomn4  21018  zntoslem  21917  mettri2  24715  mettri  24726  xmetrtri  24729  xmetrtri2  24730  metrtri  24731  ablomuldiv  31211  ablonnncan1  31216  nvmdi  31307  dipdi  31502  dipassr  31505  dipsubdir  31507  dipsubdi  31508  btwncomim  36993  cgr3tr4  37032  cgr3rflx  37034  colinbtwnle  37098  rngosubdi  39145  rngosubdir  39146  dmncan1  39276  dmncan2  39277  omlfh1N  40581  omlfh3N  40582  cvrnbtwn3  40599  cvrnbtwn4  40602  cvrcmp2  40607  hlatjrot  40696  cvrat3  40765  lplnribN  40874  ltrn2ateq  41503  dvalveclem  42348  mendlmod  44452  idomcanr  49776