Theorem 3adant3r2 1183

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 1170	1 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜏 ∧ 𝜒)) → 𝜃)

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

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 1089

This theorem is referenced by:  plttr  18412  latjlej2  18524  latmlem1  18539  latmlem2  18540  latledi  18547  latmlej11  18548  latmlej12  18549  ipopos  18606  grppnpcan2  19074  mulgsubdir  19154  imasrng  20204  imasring  20353  isdomn4  20738  zntoslem  21598  mettri2  24372  mettri  24383  xmetrtri  24386  xmetrtri2  24387  metrtri  24388  ablomuldiv  30584  ablonnncan1  30589  nvmdi  30680  dipdi  30875  dipassr  30878  dipsubdir  30880  dipsubdi  30881  btwncomim  35977  cgr3tr4  36016  cgr3rflx  36018  colinbtwnle  36082  rngosubdi  37905  rngosubdir  37906  dmncan1  38036  dmncan2  38037  omlfh1N  39214  omlfh3N  39215  cvrnbtwn3  39232  cvrnbtwn4  39235  cvrcmp2  39240  hlatjrot  39329  cvrat3  39399  lplnribN  39508  ltrn2ateq  40137  dvalveclem  40982  mendlmod  43150