Theorem 3adant3r2 1182

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 1119	. 2 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃)
3	2	3adantr2 1169	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  18399  latjlej2  18511  latmlem1  18526  latmlem2  18527  latledi  18534  latmlej11  18535  latmlej12  18536  ipopos  18593  grppnpcan2  19064  mulgsubdir  19144  imasrng  20194  imasring  20343  isdomn4  20732  zntoslem  21592  mettri2  24366  mettri  24377  xmetrtri  24380  xmetrtri2  24381  metrtri  24382  ablomuldiv  30580  ablonnncan1  30585  nvmdi  30676  dipdi  30871  dipassr  30874  dipsubdir  30876  dipsubdi  30877  btwncomim  35994  cgr3tr4  36033  cgr3rflx  36035  colinbtwnle  36099  rngosubdi  37931  rngosubdir  37932  dmncan1  38062  dmncan2  38063  omlfh1N  39239  omlfh3N  39240  cvrnbtwn3  39257  cvrnbtwn4  39260  cvrcmp2  39265  hlatjrot  39354  cvrat3  39424  lplnribN  39533  ltrn2ateq  40162  dvalveclem  41007  mendlmod  43177