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  18246  latjlej2  18360  latmlem1  18375  latmlem2  18376  latledi  18383  latmlej11  18384  latmlej12  18385  ipopos  18442  grppnpcan2  18947  mulgsubdir  19027  imasrng  20095  imasring  20248  isdomn4  20631  zntoslem  21493  mettri2  24256  mettri  24267  xmetrtri  24270  xmetrtri2  24271  metrtri  24272  ablomuldiv  30532  ablonnncan1  30537  nvmdi  30628  dipdi  30823  dipassr  30826  dipsubdir  30828  dipsubdi  30829  btwncomim  36055  cgr3tr4  36094  cgr3rflx  36096  colinbtwnle  36160  rngosubdi  37993  rngosubdir  37994  dmncan1  38124  dmncan2  38125  omlfh1N  39305  omlfh3N  39306  cvrnbtwn3  39323  cvrnbtwn4  39326  cvrcmp2  39331  hlatjrot  39420  cvrat3  39489  lplnribN  39598  ltrn2ateq  40227  dvalveclem  41072  mendlmod  43230