Theorem 3adant3r2 1202

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  plttr  18418  latjlej2  18532  latmlem1  18547  latmlem2  18548  latledi  18555  latmlej11  18556  latmlej12  18557  ipopos  18614  grppnpcan2  19144  mulgsubdir  19224  imasrng  20299  imasring  20458  isdomn4  20864  zntoslem  21756  mettri2  24549  mettri  24560  xmetrtri  24563  xmetrtri2  24564  metrtri  24565  ablomuldiv  30975  ablonnncan1  30980  nvmdi  31071  dipdi  31266  dipassr  31269  dipsubdir  31271  dipsubdi  31272  btwncomim  36542  cgr3tr4  36581  cgr3rflx  36583  colinbtwnle  36647  rngosubdi  38654  rngosubdir  38655  dmncan1  38785  dmncan2  38786  omlfh1N  40090  omlfh3N  40091  cvrnbtwn3  40108  cvrnbtwn4  40111  cvrcmp2  40116  hlatjrot  40205  cvrat3  40274  lplnribN  40383  ltrn2ateq  41012  dvalveclem  41857  mendlmod  43974  idomcanr  49170