Theorem 3adant3r2 1185

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 1121	. 2 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃)
3	2	3adantr2 1172	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  18300  latjlej2  18414  latmlem1  18429  latmlem2  18430  latledi  18437  latmlej11  18438  latmlej12  18439  ipopos  18496  grppnpcan2  19004  mulgsubdir  19084  imasrng  20152  imasring  20304  isdomn4  20687  zntoslem  21549  mettri2  24319  mettri  24330  xmetrtri  24333  xmetrtri2  24334  metrtri  24335  ablomuldiv  30641  ablonnncan1  30646  nvmdi  30737  dipdi  30932  dipassr  30935  dipsubdir  30937  dipsubdi  30938  btwncomim  36214  cgr3tr4  36253  cgr3rflx  36255  colinbtwnle  36319  rngosubdi  38283  rngosubdir  38284  dmncan1  38414  dmncan2  38415  omlfh1N  39721  omlfh3N  39722  cvrnbtwn3  39739  cvrnbtwn4  39742  cvrcmp2  39747  hlatjrot  39836  cvrat3  39905  lplnribN  40014  ltrn2ateq  40643  dvalveclem  41488  mendlmod  43638