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

Syntax hints:   → wi 4   ∧ wa 399   ∧ w3a 1089

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 210  df-an 400  df-3an 1091

This theorem is referenced by:  plttr  17802  latjlej2  17914  latmlem1  17929  latmlem2  17930  latledi  17937  latmlej11  17938  latmlej12  17939  ipopos  17996  grppnpcan2  18411  mulgsubdir  18485  imasring  19591  zntoslem  20475  mettri2  23193  mettri  23204  xmetrtri  23207  xmetrtri2  23208  metrtri  23209  ablomuldiv  28587  ablonnncan1  28592  nvmdi  28683  dipdi  28878  dipassr  28881  dipsubdir  28883  dipsubdi  28884  btwncomim  34001  cgr3tr4  34040  cgr3rflx  34042  colinbtwnle  34106  rngosubdi  35789  rngosubdir  35790  dmncan1  35920  dmncan2  35921  omlfh1N  36958  omlfh3N  36959  cvrnbtwn3  36976  cvrnbtwn4  36979  cvrcmp2  36984  hlatjrot  37073  cvrat3  37142  lplnribN  37251  ltrn2ateq  37880  dvalveclem  38725  isdomn4  39835  mendlmod  40662