Theorem 3adant3r2 1182

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 1119	. 2 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃)
3	2	3adantr2 1169	1 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜏 ∧ 𝜒)) → 𝜃)

Syntax hints:   → wi 4   ∧ wa 396   ∧ 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 206  df-an 397  df-3an 1088

This theorem is referenced by:  plttr  18060  latjlej2  18172  latmlem1  18187  latmlem2  18188  latledi  18195  latmlej11  18196  latmlej12  18197  ipopos  18254  grppnpcan2  18669  mulgsubdir  18743  imasring  19858  zntoslem  20764  mettri2  23494  mettri  23505  xmetrtri  23508  xmetrtri2  23509  metrtri  23510  ablomuldiv  28914  ablonnncan1  28919  nvmdi  29010  dipdi  29205  dipassr  29208  dipsubdir  29210  dipsubdi  29211  btwncomim  34315  cgr3tr4  34354  cgr3rflx  34356  colinbtwnle  34420  rngosubdi  36103  rngosubdir  36104  dmncan1  36234  dmncan2  36235  omlfh1N  37272  omlfh3N  37273  cvrnbtwn3  37290  cvrnbtwn4  37293  cvrcmp2  37298  hlatjrot  37387  cvrat3  37456  lplnribN  37565  ltrn2ateq  38194  dvalveclem  39039  isdomn4  40172  mendlmod  41018