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  18297  latjlej2  18409  latmlem1  18424  latmlem2  18425  latledi  18432  latmlej11  18433  latmlej12  18434  ipopos  18491  grppnpcan2  18919  mulgsubdir  18996  imasring  20147  isdomn4  20924  zntoslem  21118  mettri2  23854  mettri  23865  xmetrtri  23868  xmetrtri2  23869  metrtri  23870  ablomuldiv  29843  ablonnncan1  29848  nvmdi  29939  dipdi  30134  dipassr  30137  dipsubdir  30139  dipsubdi  30140  btwncomim  35054  cgr3tr4  35093  cgr3rflx  35095  colinbtwnle  35159  rngosubdi  36899  rngosubdir  36900  dmncan1  37030  dmncan2  37031  omlfh1N  38214  omlfh3N  38215  cvrnbtwn3  38232  cvrnbtwn4  38235  cvrcmp2  38240  hlatjrot  38329  cvrat3  38399  lplnribN  38508  ltrn2ateq  39137  dvalveclem  39982  mendlmod  42017  imasrng  46757