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  18275  latjlej2  18389  latmlem1  18404  latmlem2  18405  latledi  18412  latmlej11  18413  latmlej12  18414  ipopos  18471  grppnpcan2  18976  mulgsubdir  19056  imasrng  20124  imasring  20278  isdomn4  20661  zntoslem  21523  mettri2  24297  mettri  24308  xmetrtri  24311  xmetrtri2  24312  metrtri  24313  ablomuldiv  30640  ablonnncan1  30645  nvmdi  30736  dipdi  30931  dipassr  30934  dipsubdir  30936  dipsubdi  30937  btwncomim  36229  cgr3tr4  36268  cgr3rflx  36270  colinbtwnle  36334  rngosubdi  38196  rngosubdir  38197  dmncan1  38327  dmncan2  38328  omlfh1N  39634  omlfh3N  39635  cvrnbtwn3  39652  cvrnbtwn4  39655  cvrcmp2  39660  hlatjrot  39749  cvrat3  39818  lplnribN  39927  ltrn2ateq  40556  dvalveclem  41401  mendlmod  43546