Theorem 3adant3r2 1184

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

Syntax hints:   → wi 4   ∧ wa 397   ∧ w3a 1088

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 206  df-an 398  df-3an 1090

This theorem is referenced by:  plttr  18295  latjlej2  18407  latmlem1  18422  latmlem2  18423  latledi  18430  latmlej11  18431  latmlej12  18432  ipopos  18489  grppnpcan2  18917  mulgsubdir  18994  imasring  20143  isdomn4  20918  zntoslem  21112  mettri2  23847  mettri  23858  xmetrtri  23861  xmetrtri2  23862  metrtri  23863  ablomuldiv  29805  ablonnncan1  29810  nvmdi  29901  dipdi  30096  dipassr  30099  dipsubdir  30101  dipsubdi  30102  btwncomim  34985  cgr3tr4  35024  cgr3rflx  35026  colinbtwnle  35090  rngosubdi  36813  rngosubdir  36814  dmncan1  36944  dmncan2  36945  omlfh1N  38128  omlfh3N  38129  cvrnbtwn3  38146  cvrnbtwn4  38149  cvrcmp2  38154  hlatjrot  38243  cvrat3  38313  lplnribN  38422  ltrn2ateq  39051  dvalveclem  39896  mendlmod  41935  imasrng  46678