Theorem 3adant3r2 1181

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

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1085

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 396  df-3an 1087

This theorem is referenced by:  plttr  17975  latjlej2  18087  latmlem1  18102  latmlem2  18103  latledi  18110  latmlej11  18111  latmlej12  18112  ipopos  18169  grppnpcan2  18584  mulgsubdir  18658  imasring  19773  zntoslem  20676  mettri2  23402  mettri  23413  xmetrtri  23416  xmetrtri2  23417  metrtri  23418  ablomuldiv  28815  ablonnncan1  28820  nvmdi  28911  dipdi  29106  dipassr  29109  dipsubdir  29111  dipsubdi  29112  btwncomim  34242  cgr3tr4  34281  cgr3rflx  34283  colinbtwnle  34347  rngosubdi  36030  rngosubdir  36031  dmncan1  36161  dmncan2  36162  omlfh1N  37199  omlfh3N  37200  cvrnbtwn3  37217  cvrnbtwn4  37220  cvrcmp2  37225  hlatjrot  37314  cvrat3  37383  lplnribN  37492  ltrn2ateq  38121  dvalveclem  38966  isdomn4  40100  mendlmod  40934