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  18428  latjlej2  18542  latmlem1  18557  latmlem2  18558  latledi  18565  latmlej11  18566  latmlej12  18567  ipopos  18624  grppnpcan2  19157  mulgsubdir  19237  imasrng  20312  imasring  20471  isdomn4  20877  zntoslem  21769  mettri2  24567  mettri  24578  xmetrtri  24581  xmetrtri2  24582  metrtri  24583  ablomuldiv  31033  ablonnncan1  31038  nvmdi  31129  dipdi  31324  dipassr  31327  dipsubdir  31329  dipsubdi  31330  btwncomim  36593  cgr3tr4  36632  cgr3rflx  36634  colinbtwnle  36698  rngosubdi  38695  rngosubdir  38696  dmncan1  38826  dmncan2  38827  omlfh1N  40131  omlfh3N  40132  cvrnbtwn3  40149  cvrnbtwn4  40152  cvrcmp2  40157  hlatjrot  40246  cvrat3  40315  lplnribN  40424  ltrn2ateq  41053  dvalveclem  41898  mendlmod  44030  idomcanr  49263