Theorem 3adant3r2 1267

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 1258	. 2 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃)
3	2	3adantr2 1214	1 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜏 ∧ 𝜒)) → 𝜃)

Syntax hints:   → wi 4   ∧ wa 383   ∧ w3a 1031

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 196  df-an 385  df-3an 1033

This theorem is referenced by:  plttr  16793  latjlej2  16889  latmlem1  16904  latmlem2  16905  latledi  16912  latmlej11  16913  latmlej12  16914  ipopos  16983  grppnpcan2  17332  mulgsubdir  17405  imasring  18442  zntoslem  19724  mettri2  21956  mettri  21967  xmetrtri  21970  xmetrtri2  21971  metrtri  21972  ablomuldiv  26790  ablonnncan1  26796  nvmdi  26887  dipdi  27082  dipassr  27085  dipsubdir  27087  dipsubdi  27088  btwncomim  31290  cgr3tr4  31329  cgr3rflx  31331  colinbtwnle  31395  rngosubdi  32914  rngosubdir  32915  dmncan1  33045  dmncan2  33046  omlfh1N  33563  omlfh3N  33564  cvrnbtwn3  33581  cvrnbtwn4  33584  cvrcmp2  33589  hlatjrot  33677  cvrat3  33746  lplnribN  33855  ltrn2ateq  34485  dvalveclem  35332  mendlmod  36782