Theorem 3adant3r2 1184

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

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

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 1088

This theorem is referenced by:  plttr  18301  latjlej2  18413  latmlem1  18428  latmlem2  18429  latledi  18436  latmlej11  18437  latmlej12  18438  ipopos  18495  grppnpcan2  18966  mulgsubdir  19046  imasrng  20086  imasring  20239  isdomn4  20625  zntoslem  21466  mettri2  24229  mettri  24240  xmetrtri  24243  xmetrtri2  24244  metrtri  24245  ablomuldiv  30481  ablonnncan1  30486  nvmdi  30577  dipdi  30772  dipassr  30775  dipsubdir  30777  dipsubdi  30778  btwncomim  36001  cgr3tr4  36040  cgr3rflx  36042  colinbtwnle  36106  rngosubdi  37939  rngosubdir  37940  dmncan1  38070  dmncan2  38071  omlfh1N  39251  omlfh3N  39252  cvrnbtwn3  39269  cvrnbtwn4  39272  cvrcmp2  39277  hlatjrot  39366  cvrat3  39436  lplnribN  39545  ltrn2ateq  40174  dvalveclem  41019  mendlmod  43178