Theorem 3adant3r2 1178

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

Syntax hints:   → wi 4   ∧ wa 398   ∧ w3a 1082

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 209  df-an 399  df-3an 1084

This theorem is referenced by:  plttr  17572  latjlej2  17668  latmlem1  17683  latmlem2  17684  latledi  17691  latmlej11  17692  latmlej12  17693  ipopos  17762  grppnpcan2  18185  mulgsubdir  18259  imasring  19361  zntoslem  20695  mettri2  22943  mettri  22954  xmetrtri  22957  xmetrtri2  22958  metrtri  22959  ablomuldiv  28321  ablonnncan1  28326  nvmdi  28417  dipdi  28612  dipassr  28615  dipsubdir  28617  dipsubdi  28618  btwncomim  33467  cgr3tr4  33506  cgr3rflx  33508  colinbtwnle  33572  rngosubdi  35215  rngosubdir  35216  dmncan1  35346  dmncan2  35347  omlfh1N  36386  omlfh3N  36387  cvrnbtwn3  36404  cvrnbtwn4  36407  cvrcmp2  36412  hlatjrot  36501  cvrat3  36570  lplnribN  36679  ltrn2ateq  37308  dvalveclem  38153  mendlmod  39783