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  38142  rngosubdir  38143  dmncan1  38273  dmncan2  38274  omlfh1N  39514  omlfh3N  39515  cvrnbtwn3  39532  cvrnbtwn4  39535  cvrcmp2  39540  hlatjrot  39629  cvrat3  39698  lplnribN  39807  ltrn2ateq  40436  dvalveclem  41281  mendlmod  43427