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  18261  latjlej2  18375  latmlem1  18390  latmlem2  18391  latledi  18398  latmlej11  18399  latmlej12  18400  ipopos  18457  grppnpcan2  18962  mulgsubdir  19042  imasrng  20110  imasring  20264  isdomn4  20647  zntoslem  21509  mettri2  24283  mettri  24294  xmetrtri  24297  xmetrtri2  24298  metrtri  24299  ablomuldiv  30576  ablonnncan1  30581  nvmdi  30672  dipdi  30867  dipassr  30870  dipsubdir  30872  dipsubdi  30873  btwncomim  36156  cgr3tr4  36195  cgr3rflx  36197  colinbtwnle  36261  rngosubdi  38085  rngosubdir  38086  dmncan1  38216  dmncan2  38217  omlfh1N  39457  omlfh3N  39458  cvrnbtwn3  39475  cvrnbtwn4  39478  cvrcmp2  39483  hlatjrot  39572  cvrat3  39641  lplnribN  39750  ltrn2ateq  40379  dvalveclem  41224  mendlmod  43373