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  18306  latjlej2  18420  latmlem1  18435  latmlem2  18436  latledi  18443  latmlej11  18444  latmlej12  18445  ipopos  18502  grppnpcan2  19010  mulgsubdir  19090  imasrng  20158  imasring  20310  isdomn4  20693  zntoslem  21536  mettri2  24306  mettri  24317  xmetrtri  24320  xmetrtri2  24321  metrtri  24322  ablomuldiv  30623  ablonnncan1  30628  nvmdi  30719  dipdi  30914  dipassr  30917  dipsubdir  30919  dipsubdi  30920  btwncomim  36195  cgr3tr4  36234  cgr3rflx  36236  colinbtwnle  36300  rngosubdi  38266  rngosubdir  38267  dmncan1  38397  dmncan2  38398  omlfh1N  39704  omlfh3N  39705  cvrnbtwn3  39722  cvrnbtwn4  39725  cvrcmp2  39730  hlatjrot  39819  cvrat3  39888  lplnribN  39997  ltrn2ateq  40626  dvalveclem  41471  mendlmod  43617