Theorem 3adant3r2 1183

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 1170	1 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜏 ∧ 𝜒)) → 𝜃)

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

This theorem is referenced by:  plttr  18245  latjlej2  18357  latmlem1  18372  latmlem2  18373  latledi  18380  latmlej11  18381  latmlej12  18382  ipopos  18439  grppnpcan2  18855  mulgsubdir  18930  imasring  20059  zntoslem  21000  mettri2  23731  mettri  23742  xmetrtri  23745  xmetrtri2  23746  metrtri  23747  ablomuldiv  29557  ablonnncan1  29562  nvmdi  29653  dipdi  29848  dipassr  29851  dipsubdir  29853  dipsubdi  29854  btwncomim  34674  cgr3tr4  34713  cgr3rflx  34715  colinbtwnle  34779  rngosubdi  36477  rngosubdir  36478  dmncan1  36608  dmncan2  36609  omlfh1N  37793  omlfh3N  37794  cvrnbtwn3  37811  cvrnbtwn4  37814  cvrcmp2  37819  hlatjrot  37908  cvrat3  37978  lplnribN  38087  ltrn2ateq  38716  dvalveclem  39561  isdomn4  40697  mendlmod  41578