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  18263  latjlej2  18377  latmlem1  18392  latmlem2  18393  latledi  18400  latmlej11  18401  latmlej12  18402  ipopos  18459  grppnpcan2  18964  mulgsubdir  19044  imasrng  20112  imasring  20266  isdomn4  20649  zntoslem  21511  mettri2  24285  mettri  24296  xmetrtri  24299  xmetrtri2  24300  metrtri  24301  ablomuldiv  30627  ablonnncan1  30632  nvmdi  30723  dipdi  30918  dipassr  30921  dipsubdir  30923  dipsubdi  30924  btwncomim  36207  cgr3tr4  36246  cgr3rflx  36248  colinbtwnle  36312  rngosubdi  38146  rngosubdir  38147  dmncan1  38277  dmncan2  38278  omlfh1N  39518  omlfh3N  39519  cvrnbtwn3  39536  cvrnbtwn4  39539  cvrcmp2  39544  hlatjrot  39633  cvrat3  39702  lplnribN  39811  ltrn2ateq  40440  dvalveclem  41285  mendlmod  43431