Theorem 3adant3r2 1163

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

Syntax hints:   → wi 4   ∧ wa 387   ∧ w3a 1068

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 199  df-an 388  df-3an 1070

This theorem is referenced by:  plttr  17432  latjlej2  17528  latmlem1  17543  latmlem2  17544  latledi  17551  latmlej11  17552  latmlej12  17553  ipopos  17622  grppnpcan2  17974  mulgsubdir  18045  imasring  19086  zntoslem  20399  mettri2  22648  mettri  22659  xmetrtri  22662  xmetrtri2  22663  metrtri  22664  ablomuldiv  28100  ablonnncan1  28105  nvmdi  28196  dipdi  28391  dipassr  28394  dipsubdir  28396  dipsubdi  28397  btwncomim  32995  cgr3tr4  33034  cgr3rflx  33036  colinbtwnle  33100  rngosubdi  34665  rngosubdir  34666  dmncan1  34796  dmncan2  34797  omlfh1N  35839  omlfh3N  35840  cvrnbtwn3  35857  cvrnbtwn4  35860  cvrcmp2  35865  hlatjrot  35954  cvrat3  36023  lplnribN  36132  ltrn2ateq  36761  dvalveclem  37606  mendlmod  39189