Theorem 3adant3r2 1190

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

Syntax hints:   → wi 4   ∧ wa 396   ∧ w3a 1092

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 208  df-an 397  df-3an 1094

This theorem is referenced by:  plttr  18297  latjlej2  18411  latmlem1  18426  latmlem2  18427  latledi  18434  latmlej11  18435  latmlej12  18436  ipopos  18493  grppnpcan2  19001  mulgsubdir  19081  imasrng  20149  imasring  20301  isdomn4  20688  zntoslem  21531  mettri2  24324  mettri  24335  xmetrtri  24338  xmetrtri2  24339  metrtri  24340  ablomuldiv  30641  ablonnncan1  30646  nvmdi  30737  dipdi  30932  dipassr  30935  dipsubdir  30937  dipsubdi  30938  btwncomim  36241  cgr3tr4  36280  cgr3rflx  36282  colinbtwnle  36346  rngosubdi  38312  rngosubdir  38313  dmncan1  38443  dmncan2  38444  omlfh1N  39750  omlfh3N  39751  cvrnbtwn3  39768  cvrnbtwn4  39771  cvrcmp2  39776  hlatjrot  39865  cvrat3  39934  lplnribN  40043  ltrn2ateq  40672  dvalveclem  41517  mendlmod  43634