Theorem 3adant3r2 1275

Description: Deduction adding a conjunct to antecedent. (Contributed by NM, 17-Feb-2008.)

Hypothesis

Ref	Expression
3exp.1	⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)

Assertion

Ref	Expression
3adant3r2	⊢ ((𝜑 ∧ (𝜓 ∧ 𝜏 ∧ 𝜒)) → 𝜃)

Proof of Theorem 3adant3r2

Step	Hyp	Ref	Expression
1		3exp.1	. . 3 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)
2	1	3expb 1266	. 2 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃)
3	2	3adantr2 1221	1 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜏 ∧ 𝜒)) → 𝜃)

Syntax hints:   → wi 4   ∧ wa 384   ∧ w3a 1037

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 197  df-an 386  df-3an 1039

This theorem is referenced by:  plttr  16970  latjlej2  17066  latmlem1  17081  latmlem2  17082  latledi  17089  latmlej11  17090  latmlej12  17091  ipopos  17160  grppnpcan2  17509  mulgsubdir  17582  imasring  18619  zntoslem  19905  mettri2  22146  mettri  22157  xmetrtri  22160  xmetrtri2  22161  metrtri  22162  ablomuldiv  27406  ablonnncan1  27412  nvmdi  27503  dipdi  27698  dipassr  27701  dipsubdir  27703  dipsubdi  27704  btwncomim  32120  cgr3tr4  32159  cgr3rflx  32161  colinbtwnle  32225  rngosubdi  33744  rngosubdir  33745  dmncan1  33875  dmncan2  33876  omlfh1N  34545  omlfh3N  34546  cvrnbtwn3  34563  cvrnbtwn4  34566  cvrcmp2  34571  hlatjrot  34659  cvrat3  34728  lplnribN  34837  ltrn2ateq  35467  dvalveclem  36314  mendlmod  37763